assump C |- X <= X in C lambda C |- X <= C |- Y and can beta/nu convert X and Y xi C |- YZ <= C |- XZ; C |- #XY deduce C |- #XY <= C,Xa |- Ya; C |- H(Xa); a not free in C, X, or Y. xiprop C |- H(#XY) <= C |- H(Xa); C,Xa |- H(Ya); a not free in C, X, or Y. prop C |- H(HX) equal C |- A <= C |- B, B can be converted to A via definition substitution of terms without capturing bound variables K = \x y: x (=>) = \X Y: #(KX)(KY) (.) = \f g x: f (g x) (->) = \A B f: #A(B . f) True = #HH U = K True L = U -> H Nat = \x. #L(\p: p 0 => #U(\n: p n => p (S n)) => p x) assump: La, K(a 0)b, K(#U(\n: a n => a (S n)))c |- K(a 0)b equal: La, K(a 0)b, K(#U(\n: a n => a (S n)))c |- (\x y: x)(a 0)b lambda: La, K(a 0)b, K(#U(\n: a n => a (S n)))c |- (\x y: x)(a 0)c 13 equal: La, K(a 0)b, K(#U(\n: a n => a (S n)))c |- K(a 0)c 12 assump: La, K(a 0)b, Uc, K(a c)e, Hf |- Hf prop: La, K(a 0)b, Uc, K(a c)e |- H(Hf) deduce 12: La, K(a 0)b, Uc, K(a c)e |- #HH lambda: La, K(a 0)b, Uc, K(a c)e |- (\x y: x) (#HH) (S c) equal: La, K(a 0)b, Uc, K(a c)e |- K True (S c) 11 equal: La, K(a 0)b, Uc, K(a c)e |- U(S c) assump: La, K(a 0)b, Uc, K(a c)e |- L a equal: La, K(a 0)b, Uc, K(a c)e |- (U -> H) a equal: La, K(a 0)b, Uc, K(a c)e |- (\X Y f: #A(B.f)) U H a lambda: La, K(a 0)b, Uc, K(a c)e |- #U(H.a) xi 11: La, K(a 0)b, Uc, K(a c)e |- (H.a)(S c) equal: La, K(a 0)b, Uc, K(a c)e |- (\x. H(a x))(S c) lambda: La, K(a 0)b, Uc, K(a c)e |- H(a (S c)) lambda: La, K(a 0)b, Uc, K(a c)e |- H((\x y: x) (a (S c)) e) 10 equal: La, K(a 0)b, Uc, K(a c)e |- H(K (a (S c)) e) assump: La, K(a 0)b, Uc |- L a equal: La, K(a 0)b, Uc |- (U -> H) a equal: La, K(a 0)b, Uc |- (\A B f: #A(B.f)) U H a lambda: La, K(a 0)b, Uc |- #U(H.a) 9 equal: La, K(a 0)b, Uc |- #(K True)(\x: H(a x)) assump: La, K(a 0)b, Uc |- U c equal: La, K(a 0)b, Uc |- K True c xi 9: La, K(a 0)b, Uc |- (\x: H (a x)) c lambda: La, K(a 0)b, Uc |- H((\x y: x) (a c) e) equal: La, K(a 0)b, Uc |- H(K (a c) e) xiprop 10: La, K(a 0)b, Uc |- H(#(K (a c))(K (a (S c)))) lambda: La, K(a 0)b, Uc |- H((\X Y: #(K X)(K Y)) (a c) (a (S c))) equal: La, K(a 0)b, Uc |- H(a c => a (S c))) 8 lambda: La, K(a 0)b, Uc |- H((\n: a n => a (S n))c) 7 prop La, K(a 0)b, Hd |- H(Hd) prop La, K(a 0)b |- H(Hd) xiprop 7: La, K(a 0)b |- H(#HH) lambda: La, K(a 0)b |- H((\x y: x) (#HH) c) equal: La, K(a 0)b |- H(K True c) equal: La, K(a 0)b |- H(Uc) xiprop 8: La, K(a 0)b |- H(#U(\n: a n => a (S n))) lambda: La, K(a 0)b |- H((\x y: x)(#U(\n: a n => a (S n)))c) equal: La, K(a 0)b |- H(K(#U(\n: a n => a (S n)))c) 6 deduce 13: La, K(a 0)b |- #(K(#U(\n: a n => a (S n))))(K(a 0)) assump: La |- La equal: La |- (U -> H)a equal: La |- (\f: #U(H.f))a lambda: La |- #U(H.a) 5 equal: La |- #(K True)(\x. H(a x)) 4 assump La,Hb |- Hb prop La |- H(Hb) deduce 4: La |- #HH lambda: La |- (\x y: x) (#HH) 0 equal: La |- K True 0 xi 5: La |- (\x: H (a x)) 0 lambda: La |- H((\x y: x)(a 0) b) equal: La |- H(K(a 0)b) deduce 6: La |- #(K(a 0))(#(K(#U(\n: a n => a (S n))))(K(a 0))) equal: La |- a 0 => #U(\n: a n => a (S n)) => a 0 3 lambda: La |- (\p: p 0 => #U(\n: p n => p (S n)) => p 0) a prop: Ub |- H(H(a b)) 2 lambda: Ub |- H((\x.H(a x))b) 1 prop: Hc |- H(Hc) prop: |- H(Hc) xiprop 1: |- H(#HH) equal: |- H(True) lambda: |- H((\x y: x) True b) equal: |- H(K True b) equal: |- H(Ub) xiprop 2: |- H(#U(\x: H(a x))) equal: |- H(#U(H.a)) lambda: |- H((\f: #U(H.f))a) equal: |- H((U -> H)a) equal: |- H(La) deduce 3: |- #L(\p: p 0 => #U(\n: p n => p (S n)) => p 0) lambda: |- (\x: #L(\p: p 0 => #U(\n: p n => p (S n)) => p x)) 0 equal: |- Nat 0