DEFINITION csubst0_clear_S()
TYPE =
∀c1:C
.∀c2:C
.∀v:T
.∀i:nat
.csubst0 (S i) v c1 c2
→∀c:C
.clear c1 c
→(or4
clear c2 c
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2)
BODY =
assume c1: C
we proceed by induction on c1 to prove
∀c2:C
.∀v:T
.∀i:nat
.csubst0 (S i) v c1 c2
→∀c0:C
.clear c1 c0
→(or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2)
case CSort : n:nat ⇒
the thesis becomes
∀c2:C
.∀v:T
.∀i:nat
.∀H:csubst0 (S i) v (CSort n) c2
.∀c:C
.clear (CSort n) c
→(or4
clear c2 c
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2)
assume c2: C
assume v: T
assume i: nat
suppose H: csubst0 (S i) v (CSort n) c2
assume c: C
suppose : clear (CSort n) c
by (csubst0_gen_sort . . . . H .)
we proved
or4
clear c2 c
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
∀c2:C
.∀v:T
.∀i:nat
.∀H:csubst0 (S i) v (CSort n) c2
.∀c:C
.clear (CSort n) c
→(or4
clear c2 c
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2)
case CHead : c:C k:K t:T ⇒
the thesis becomes
∀c2:C
.∀v:T
.∀i:nat
.∀H0:csubst0 (S i) v (CHead c k t) c2
.∀c0:C
.∀H1:clear (CHead c k t) c0
.or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
(H) by induction hypothesis we know
∀c2:C
.∀v:T
.∀i:nat
.csubst0 (S i) v c c2
→∀c0:C
.clear c c0
→(or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2)
assume c2: C
assume v: T
assume i: nat
suppose H0: csubst0 (S i) v (CHead c k t) c2
assume c0: C
suppose H1: clear (CHead c k t) c0
by (csubst0_gen_head . . . . . . H0)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (S i) (s k j)
λu2:T.λ:nat.eq C c2 (CHead c k u2)
λu2:T.λj:nat.subst0 j v t u2
ex3_2
C
nat
λ:C.λj:nat.eq nat (S i) (s k j)
λc2:C.λ:nat.eq C c2 (CHead c2 k t)
λc2:C.λj:nat.csubst0 j v c c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (S i) (s k j)
λu2:T.λc2:C.λ:nat.eq C c2 (CHead c2 k u2)
λu2:T.λ:C.λj:nat.subst0 j v t u2
λ:T.λc2:C.λj:nat.csubst0 j v c c2
we proceed by induction on the previous result to prove
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case or3_intro0 : H2:ex3_2 T nat λ:T.λj:nat.eq nat (S i) (s k j) λu2:T.λ:nat.eq C c2 (CHead c k u2) λu2:T.λj:nat.subst0 j v t u2 ⇒
the thesis becomes
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proceed by induction on H2 to prove
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case ex3_2_intro : x0:T x1:nat H3:eq nat (S i) (s k x1) H4:eq C c2 (CHead c k x0) H5:subst0 x1 v t x0 ⇒
the thesis becomes
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
assume b: B
suppose H6: clear (CHead c (Bind b) t) c0
suppose H7: eq nat (S i) (s (Bind b) x1)
(H8)
consider H7
we proved eq nat (S i) (s (Bind b) x1)
that is equivalent to eq nat (S i) (S x1)
by (f_equal . . . . . previous)
we proved
eq
nat
<λ:nat.nat> CASE S i OF O⇒i | S n⇒n
<λ:nat.nat> CASE S x1 OF O⇒i | S n⇒n
eq
nat
λe:nat.<λ:nat.nat> CASE e OF O⇒i | S n⇒n (S i)
λe:nat.<λ:nat.nat> CASE e OF O⇒i | S n⇒n (S x1)
end of H8
(H9)
consider H8
we proved
eq
nat
<λ:nat.nat> CASE S i OF O⇒i | S n⇒n
<λ:nat.nat> CASE S x1 OF O⇒i | S n⇒n
that is equivalent to eq nat i x1
by (eq_ind_r . . . H5 . previous)
subst0 i v t x0
end of H9
(h1)
(h1)
by (refl_equal . .)
eq C (CHead c (Bind b) t) (CHead c (Bind b) t)
end of h1
(h2)
by (clear_bind . . .)
clear (CHead c (Bind b) x0) (CHead c (Bind b) x0)
end of h2
by (ex3_4_intro . . . . . . . . . . . h1 h2 H9)
we proved
ex3_4
B
C
T
T
λb0:B.λe:C.λu1:T.λ:T.eq C (CHead c (Bind b) t) (CHead e (Bind b0) u1)
λb0:B.λe:C.λ:T.λu2:T.clear (CHead c (Bind b) x0) (CHead e (Bind b0) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
by (or4_intro1 . . . . previous)
or4
clear (CHead c (Bind b) x0) (CHead c (Bind b) t)
ex3_4
B
C
T
T
λb0:B.λe:C.λu1:T.λ:T.eq C (CHead c (Bind b) t) (CHead e (Bind b0) u1)
λb0:B.λe:C.λ:T.λu2:T.clear (CHead c (Bind b) x0) (CHead e (Bind b0) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C (CHead c (Bind b) t) (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.clear (CHead c (Bind b) x0) (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu1:T.λ:T.eq C (CHead c (Bind b) t) (CHead e1 (Bind b0) u1)
λb0:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead c (Bind b) x0) (CHead e2 (Bind b0) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
end of h1
(h2)
by (clear_gen_bind . . . . H6)
eq C c0 (CHead c (Bind b) t)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or4
clear (CHead c (Bind b) x0) c0
ex3_4
B
C
T
T
λb0:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b0) u1)
λb0:B.λe:C.λ:T.λu2:T.clear (CHead c (Bind b) x0) (CHead e (Bind b0) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.clear (CHead c (Bind b) x0) (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b0) u1)
λb0:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead c (Bind b) x0) (CHead e2 (Bind b0) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
∀H6:clear (CHead c (Bind b) t) c0
.∀H7:eq nat (S i) (s (Bind b) x1)
.or4
clear (CHead c (Bind b) x0) c0
ex3_4
B
C
T
T
λb0:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b0) u1)
λb0:B.λe:C.λ:T.λu2:T.clear (CHead c (Bind b) x0) (CHead e (Bind b0) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.clear (CHead c (Bind b) x0) (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b0) u1)
λb0:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead c (Bind b) x0) (CHead e2 (Bind b0) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
assume f: F
suppose H6: clear (CHead c (Flat f) t) c0
suppose H7: eq nat (S i) (s (Flat f) x1)
(H8)
by (f_equal . . . . . H7)
we proved eq nat (S i) (s (Flat f) x1)
eq nat (λe:nat.e (S i)) (λe:nat.e (s (Flat f) x1))
end of H8
by (clear_gen_flat . . . . H6)
we proved clear c c0
by (clear_flat . . previous . .)
we proved clear (CHead c (Flat f) x0) c0
by (or4_intro0 . . . . previous)
we proved
or4
clear (CHead c (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead c (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead c (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead c (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
∀H6:clear (CHead c (Flat f) t) c0
.∀H7:eq nat (S i) (s (Flat f) x1)
.or4
clear (CHead c (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead c (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead c (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead c (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (previous . H1 H3)
we proved
or4
clear (CHead c k x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead c k x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead c k x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead c k x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (eq_ind_r . . . previous . H4)
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case or3_intro1 : H2:ex3_2 C nat λ:C.λj:nat.eq nat (S i) (s k j) λc3:C.λ:nat.eq C c2 (CHead c3 k t) λc3:C.λj:nat.csubst0 j v c c3 ⇒
the thesis becomes
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proceed by induction on H2 to prove
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case ex3_2_intro : x0:C x1:nat H3:eq nat (S i) (s k x1) H4:eq C c2 (CHead x0 k t) H5:csubst0 x1 v c x0 ⇒
the thesis becomes
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
assume b: B
suppose H6: clear (CHead c (Bind b) t) c0
suppose H7: eq nat (S i) (s (Bind b) x1)
(H8)
consider H7
we proved eq nat (S i) (s (Bind b) x1)
that is equivalent to eq nat (S i) (S x1)
by (f_equal . . . . . previous)
we proved
eq
nat
<λ:nat.nat> CASE S i OF O⇒i | S n⇒n
<λ:nat.nat> CASE S x1 OF O⇒i | S n⇒n
eq
nat
λe:nat.<λ:nat.nat> CASE e OF O⇒i | S n⇒n (S i)
λe:nat.<λ:nat.nat> CASE e OF O⇒i | S n⇒n (S x1)
end of H8
(H9)
consider H8
we proved
eq
nat
<λ:nat.nat> CASE S i OF O⇒i | S n⇒n
<λ:nat.nat> CASE S x1 OF O⇒i | S n⇒n
that is equivalent to eq nat i x1
by (eq_ind_r . . . H5 . previous)
csubst0 i v c x0
end of H9
(h1)
(h1)
by (refl_equal . .)
eq C (CHead c (Bind b) t) (CHead c (Bind b) t)
end of h1
(h2)
by (clear_bind . . .)
clear (CHead x0 (Bind b) t) (CHead x0 (Bind b) t)
end of h2
by (ex3_4_intro . . . . . . . . . . . h1 h2 H9)
we proved
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C (CHead c (Bind b) t) (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Bind b) t) (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
by (or4_intro2 . . . . previous)
or4
clear (CHead x0 (Bind b) t) (CHead c (Bind b) t)
ex3_4
B
C
T
T
λb0:B.λe:C.λu1:T.λ:T.eq C (CHead c (Bind b) t) (CHead e (Bind b0) u1)
λb0:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Bind b) t) (CHead e (Bind b0) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C (CHead c (Bind b) t) (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Bind b) t) (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu1:T.λ:T.eq C (CHead c (Bind b) t) (CHead e1 (Bind b0) u1)
λb0:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Bind b) t) (CHead e2 (Bind b0) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
end of h1
(h2)
by (clear_gen_bind . . . . H6)
eq C c0 (CHead c (Bind b) t)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or4
clear (CHead x0 (Bind b) t) c0
ex3_4
B
C
T
T
λb0:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b0) u1)
λb0:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Bind b) t) (CHead e (Bind b0) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Bind b) t) (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b0) u1)
λb0:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Bind b) t) (CHead e2 (Bind b0) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
∀H6:clear (CHead c (Bind b) t) c0
.∀H7:eq nat (S i) (s (Bind b) x1)
.or4
clear (CHead x0 (Bind b) t) c0
ex3_4
B
C
T
T
λb0:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b0) u1)
λb0:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Bind b) t) (CHead e (Bind b0) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Bind b) t) (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b0) u1)
λb0:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Bind b) t) (CHead e2 (Bind b0) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
assume f: F
suppose H6: clear (CHead c (Flat f) t) c0
suppose H7: eq nat (S i) (s (Flat f) x1)
(H8)
by (f_equal . . . . . H7)
we proved eq nat (S i) (s (Flat f) x1)
eq nat (λe:nat.e (S i)) (λe:nat.e (s (Flat f) x1))
end of H8
(H9)
consider H8
we proved eq nat (S i) (s (Flat f) x1)
that is equivalent to eq nat (S i) x1
by (eq_ind_r . . . H5 . previous)
csubst0 (S i) v c x0
end of H9
(H10)
by (clear_gen_flat . . . . H6)
we proved clear c c0
by (H . . . H9 . previous)
or4
clear x0 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear x0 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear x0 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear x0 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
end of H10
we proceed by induction on H10 to prove
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case or4_intro0 : H11:clear x0 c0 ⇒
the thesis becomes
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (clear_flat . . H11 . .)
we proved clear (CHead x0 (Flat f) t) c0
by (or4_intro0 . . . . previous)
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case or4_intro1 : H11:ex3_4 B C T T λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1) λb:B.λe:C.λ:T.λu2:T.clear x0 (CHead e (Bind b) u2) λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2 ⇒
the thesis becomes
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proceed by induction on H11 to prove
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case ex3_4_intro : x2:B x3:C x4:T x5:T H12:eq C c0 (CHead x3 (Bind x2) x4) H13:clear x0 (CHead x3 (Bind x2) x5) H14:subst0 i v x4 x5 ⇒
the thesis becomes
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (clear_flat . . H13 . .)
we proved clear (CHead x0 (Flat f) t) (CHead x3 (Bind x2) x5)
by (ex3_4_intro . . . . . . . . . . . H12 previous H14)
we proved
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
by (or4_intro1 . . . . previous)
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case or4_intro2 : H11:ex3_4 B C C T λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u) λb:B.λ:C.λe2:C.λu:T.clear x0 (CHead e2 (Bind b) u) λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2 ⇒
the thesis becomes
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proceed by induction on H11 to prove
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case ex3_4_intro : x2:B x3:C x4:C x5:T H12:eq C c0 (CHead x3 (Bind x2) x5) H13:clear x0 (CHead x4 (Bind x2) x5) H14:csubst0 i v x3 x4 ⇒
the thesis becomes
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (clear_flat . . H13 . .)
we proved clear (CHead x0 (Flat f) t) (CHead x4 (Bind x2) x5)
by (ex3_4_intro . . . . . . . . . . . H12 previous H14)
we proved
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
by (or4_intro2 . . . . previous)
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case or4_intro3 : H11:ex4_5 B C C T T λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1) λb:B.λ:C.λe2:C.λ:T.λu2:T.clear x0 (CHead e2 (Bind b) u2) λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2 λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2 ⇒
the thesis becomes
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proceed by induction on H11 to prove
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case ex4_5_intro : x2:B x3:C x4:C x5:T x6:T H12:eq C c0 (CHead x3 (Bind x2) x5) H13:clear x0 (CHead x4 (Bind x2) x6) H14:subst0 i v x5 x6 H15:csubst0 i v x3 x4 ⇒
the thesis becomes
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (clear_flat . . H13 . .)
we proved clear (CHead x0 (Flat f) t) (CHead x4 (Bind x2) x6)
by (ex4_5_intro . . . . . . . . . . . . . . H12 previous H14 H15)
we proved
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (or4_intro3 . . . . previous)
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proved
or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
∀H6:clear (CHead c (Flat f) t) c0
.∀H7:eq nat (S i) (s (Flat f) x1)
.or4
clear (CHead x0 (Flat f) t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 (Flat f) t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (previous . H1 H3)
we proved
or4
clear (CHead x0 k t) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x0 k t) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x0 k t) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x0 k t) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (eq_ind_r . . . previous . H4)
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case or3_intro2 : H2:ex4_3 T C nat λ:T.λ:C.λj:nat.eq nat (S i) (s k j) λu2:T.λc3:C.λ:nat.eq C c2 (CHead c3 k u2) λu2:T.λ:C.λj:nat.subst0 j v t u2 λ:T.λc3:C.λj:nat.csubst0 j v c c3 ⇒
the thesis becomes
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proceed by induction on H2 to prove
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case ex4_3_intro : x0:T x1:C x2:nat H3:eq nat (S i) (s k x2) H4:eq C c2 (CHead x1 k x0) H5:subst0 x2 v t x0 H6:csubst0 x2 v c x1 ⇒
the thesis becomes
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
assume b: B
suppose H7: clear (CHead c (Bind b) t) c0
suppose H8: eq nat (S i) (s (Bind b) x2)
(H9)
consider H8
we proved eq nat (S i) (s (Bind b) x2)
that is equivalent to eq nat (S i) (S x2)
by (f_equal . . . . . previous)
we proved
eq
nat
<λ:nat.nat> CASE S i OF O⇒i | S n⇒n
<λ:nat.nat> CASE S x2 OF O⇒i | S n⇒n
eq
nat
λe:nat.<λ:nat.nat> CASE e OF O⇒i | S n⇒n (S i)
λe:nat.<λ:nat.nat> CASE e OF O⇒i | S n⇒n (S x2)
end of H9
(H10)
consider H9
we proved
eq
nat
<λ:nat.nat> CASE S i OF O⇒i | S n⇒n
<λ:nat.nat> CASE S x2 OF O⇒i | S n⇒n
that is equivalent to eq nat i x2
by (eq_ind_r . . . H6 . previous)
csubst0 i v c x1
end of H10
(H11)
consider H9
we proved
eq
nat
<λ:nat.nat> CASE S i OF O⇒i | S n⇒n
<λ:nat.nat> CASE S x2 OF O⇒i | S n⇒n
that is equivalent to eq nat i x2
by (eq_ind_r . . . H5 . previous)
subst0 i v t x0
end of H11
(h1)
(h1)
by (refl_equal . .)
eq C (CHead c (Bind b) t) (CHead c (Bind b) t)
end of h1
(h2)
by (clear_bind . . .)
clear (CHead x1 (Bind b) x0) (CHead x1 (Bind b) x0)
end of h2
by (ex4_5_intro . . . . . . . . . . . . . . h1 h2 H11 H10)
we proved
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu1:T.λ:T.eq C (CHead c (Bind b) t) (CHead e1 (Bind b0) u1)
λb0:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Bind b) x0) (CHead e2 (Bind b0) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (or4_intro3 . . . . previous)
or4
clear (CHead x1 (Bind b) x0) (CHead c (Bind b) t)
ex3_4
B
C
T
T
λb0:B.λe:C.λu1:T.λ:T.eq C (CHead c (Bind b) t) (CHead e (Bind b0) u1)
λb0:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Bind b) x0) (CHead e (Bind b0) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C (CHead c (Bind b) t) (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Bind b) x0) (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu1:T.λ:T.eq C (CHead c (Bind b) t) (CHead e1 (Bind b0) u1)
λb0:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Bind b) x0) (CHead e2 (Bind b0) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
end of h1
(h2)
by (clear_gen_bind . . . . H7)
eq C c0 (CHead c (Bind b) t)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or4
clear (CHead x1 (Bind b) x0) c0
ex3_4
B
C
T
T
λb0:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b0) u1)
λb0:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Bind b) x0) (CHead e (Bind b0) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Bind b) x0) (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b0) u1)
λb0:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Bind b) x0) (CHead e2 (Bind b0) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
∀H7:clear (CHead c (Bind b) t) c0
.∀H8:eq nat (S i) (s (Bind b) x2)
.or4
clear (CHead x1 (Bind b) x0) c0
ex3_4
B
C
T
T
λb0:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b0) u1)
λb0:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Bind b) x0) (CHead e (Bind b0) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Bind b) x0) (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b0) u1)
λb0:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Bind b) x0) (CHead e2 (Bind b0) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
assume f: F
suppose H7: clear (CHead c (Flat f) t) c0
suppose H8: eq nat (S i) (s (Flat f) x2)
(H9)
by (f_equal . . . . . H8)
we proved eq nat (S i) (s (Flat f) x2)
eq nat (λe:nat.e (S i)) (λe:nat.e (s (Flat f) x2))
end of H9
(H10)
consider H9
we proved eq nat (S i) (s (Flat f) x2)
that is equivalent to eq nat (S i) x2
by (eq_ind_r . . . H6 . previous)
csubst0 (S i) v c x1
end of H10
(H12)
by (clear_gen_flat . . . . H7)
we proved clear c c0
by (H . . . H10 . previous)
or4
clear x1 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear x1 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear x1 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear x1 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
end of H12
we proceed by induction on H12 to prove
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case or4_intro0 : H13:clear x1 c0 ⇒
the thesis becomes
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (clear_flat . . H13 . .)
we proved clear (CHead x1 (Flat f) x0) c0
by (or4_intro0 . . . . previous)
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case or4_intro1 : H13:ex3_4 B C T T λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1) λb:B.λe:C.λ:T.λu2:T.clear x1 (CHead e (Bind b) u2) λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2 ⇒
the thesis becomes
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proceed by induction on H13 to prove
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case ex3_4_intro : x3:B x4:C x5:T x6:T H14:eq C c0 (CHead x4 (Bind x3) x5) H15:clear x1 (CHead x4 (Bind x3) x6) H16:subst0 i v x5 x6 ⇒
the thesis becomes
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (clear_flat . . H15 . .)
we proved clear (CHead x1 (Flat f) x0) (CHead x4 (Bind x3) x6)
by (ex3_4_intro . . . . . . . . . . . H14 previous H16)
we proved
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
by (or4_intro1 . . . . previous)
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case or4_intro2 : H13:ex3_4 B C C T λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u) λb:B.λ:C.λe2:C.λu:T.clear x1 (CHead e2 (Bind b) u) λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2 ⇒
the thesis becomes
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proceed by induction on H13 to prove
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case ex3_4_intro : x3:B x4:C x5:C x6:T H14:eq C c0 (CHead x4 (Bind x3) x6) H15:clear x1 (CHead x5 (Bind x3) x6) H16:csubst0 i v x4 x5 ⇒
the thesis becomes
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (clear_flat . . H15 . .)
we proved clear (CHead x1 (Flat f) x0) (CHead x5 (Bind x3) x6)
by (ex3_4_intro . . . . . . . . . . . H14 previous H16)
we proved
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
by (or4_intro2 . . . . previous)
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case or4_intro3 : H13:ex4_5 B C C T T λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1) λb:B.λ:C.λe2:C.λ:T.λu2:T.clear x1 (CHead e2 (Bind b) u2) λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2 λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2 ⇒
the thesis becomes
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proceed by induction on H13 to prove
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
case ex4_5_intro : x3:B x4:C x5:C x6:T x7:T H14:eq C c0 (CHead x4 (Bind x3) x6) H15:clear x1 (CHead x5 (Bind x3) x7) H16:subst0 i v x6 x7 H17:csubst0 i v x4 x5 ⇒
the thesis becomes
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (clear_flat . . H15 . .)
we proved clear (CHead x1 (Flat f) x0) (CHead x5 (Bind x3) x7)
by (ex4_5_intro . . . . . . . . . . . . . . H14 previous H16 H17)
we proved
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (or4_intro3 . . . . previous)
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proved
or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
∀H7:clear (CHead c (Flat f) t) c0
.∀H8:eq nat (S i) (s (Flat f) x2)
.or4
clear (CHead x1 (Flat f) x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 (Flat f) x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (previous . H1 H3)
we proved
or4
clear (CHead x1 k x0) c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear (CHead x1 k x0) (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear (CHead x1 k x0) (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear (CHead x1 k x0) (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
by (eq_ind_r . . . previous . H4)
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proved
or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
∀c2:C
.∀v:T
.∀i:nat
.∀H0:csubst0 (S i) v (CHead c k t) c2
.∀c0:C
.∀H1:clear (CHead c k t) c0
.or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2
we proved
∀c2:C
.∀v:T
.∀i:nat
.csubst0 (S i) v c1 c2
→∀c0:C
.clear c1 c0
→(or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2)
we proved
∀c1:C
.∀c2:C
.∀v:T
.∀i:nat
.csubst0 (S i) v c1 c2
→∀c0:C
.clear c1 c0
→(or4
clear c2 c0
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C c0 (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C c0 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c0 (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2)