例えば、今回はA→Aの具体項をS,Kコンビネータとβ簡約によって得られたが、
同様に
公理S:(A→(A→A)→A)→(A→A→A)→A→A
公理K:A→(A→A)→A
推論規則 (A→A→A)→A→A
公理K:A→A→A
推論規則 A→A
によってA→Aが示せることがわかる。

ここから、
A,A→A,A型によるSコンビネータ
A,A→A型によるKコンビネータ
A,A型によるKコンビネータ
を用いたλ項
(S:(A→(A→A)→A)→(A→A→A)→A→A)(K:A→(A→A)→A)(K:A→A→A)
を簡約すると、
(SK:(A→A→A)→A→A)(K:A→A→A)
(SKK:A→A)
のようになり、A→A型の具体項が得られる。
ところで、λ項の型だけに注目すると、
S,Kコンビネータはヒルベルト流命題論理の公理に、β簡約は推論規則に対応している。
つまり、型だけ見ればβ簡約により証明の流れを見ることができる。

なお、S,KはX,Y,A,B,Cがどのような型であってもよい。(正確には、どの型の組み合わせにも対応するSコンビネータとKコンビネータが存在する。)
また、SKKaは簡約を繰り返すことでaとなるので、SKKは恒等関数である。
aの型をAとして、SKKaの型を推論すると、
(S:(A→(A→A)→A)→(A→A→A)→A→A)(K:A→(A→A)→A)(K:A→A→A)(a:A)となり、簡約を進めると、
(K:A→(A→A)→A)(a:A)((K:A→A→A)(a:A))
(a:A)
となる。