DEFINITION csubst0_getl_lt()
TYPE =
∀i:nat
.∀n:nat
.lt n i
→∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e:C
.getl n c1 e
→(or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2)
BODY =
assume i: nat
assume n: nat
suppose H: lt n i
assume c1: C
assume c2: C
assume v: T
suppose H0: csubst0 i v c1 c2
assume e: C
suppose H1: getl n c1 e
(H2)
by (getl_gen_all . . . H1)
ex2 C λe:C.drop n O c1 e λe:C.clear e e
end of H2
we proceed by induction on H2 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case ex_intro2 : x:C H3:drop n O c1 x H4:clear x e ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
(H5)
by (csubst0_drop_lt . . H . . . H0 . H3)
or4
drop n O c2 x
ex3_4
K
C
T
T
λk:K.λe0:C.λu:T.λ:T.eq C x (CHead e0 k u)
λk:K.λe0:C.λ:T.λw:T.drop n O c2 (CHead e0 k w)
λk:K.λ:C.λu:T.λw:T.subst0 (minus i (s k n)) v u w
ex3_4
K
C
C
T
λk:K.λe1:C.λ:C.λu:T.eq C x (CHead e1 k u)
λk:K.λ:C.λe2:C.λu:T.drop n O c2 (CHead e2 k u)
λk:K.λe1:C.λe2:C.λ:T.csubst0 (minus i (s k n)) v e1 e2
ex4_5
K
C
C
T
T
λk:K.λe1:C.λ:C.λu:T.λ:T.eq C x (CHead e1 k u)
λk:K.λ:C.λe2:C.λ:T.λw:T.drop n O c2 (CHead e2 k w)
λk:K.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (s k n)) v u w
λk:K.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (s k n)) v e1 e2
end of H5
we proceed by induction on H5 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case or4_intro0 : H6:drop n O c2 x ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (getl_intro . . . . H6 H4)
we proved getl n c2 e
by (or4_intro0 . . . . previous)
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case or4_intro1 : H6:ex3_4 K C T T λk:K.λe0:C.λu:T.λ:T.eq C x (CHead e0 k u) λk:K.λe0:C.λ:T.λw:T.drop n O c2 (CHead e0 k w) λk:K.λ:C.λu:T.λw:T.subst0 (minus i (s k n)) v u w ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proceed by induction on H6 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case ex3_4_intro : x0:K x1:C x2:T x3:T H7:eq C x (CHead x1 x0 x2) H8:drop n O c2 (CHead x1 x0 x3) H9:subst0 (minus i (s x0 n)) v x2 x3 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
(H10)
we proceed by induction on H7 to prove clear (CHead x1 x0 x2) e
case refl_equal : ⇒
the thesis becomes the hypothesis H4
clear (CHead x1 x0 x2) e
end of H10
assume b: B
suppose H11: drop n O c2 (CHead x1 (Bind b) x3)
suppose H12: subst0 (minus i (s (Bind b) n)) v x2 x3
suppose H13: clear (CHead x1 (Bind b) x2) e
(h1)
(h1)
by (refl_equal . .)
eq C (CHead x1 (Bind b) x2) (CHead x1 (Bind b) x2)
end of h1
(h2)
by (clear_bind . . .)
we proved clear (CHead x1 (Bind b) x3) (CHead x1 (Bind b) x3)
by (getl_intro . . . . H11 previous)
getl n c2 (CHead x1 (Bind b) x3)
end of h2
(h3)
consider H12
we proved subst0 (minus i (s (Bind b) n)) v x2 x3
subst0 (minus i (S n)) v x2 x3
end of h3
by (ex3_4_intro . . . . . . . . . . . h1 h2 h3)
we proved
ex3_4
B
C
T
T
λb0:B.λe0:C.λu:T.λ:T.eq C (CHead x1 (Bind b) x2) (CHead e0 (Bind b0) u)
λb0:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b0) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
by (or4_intro1 . . . . previous)
or4
getl n c2 (CHead x1 (Bind b) x2)
ex3_4
B
C
T
T
λb0:B.λe0:C.λu:T.λ:T.eq C (CHead x1 (Bind b) x2) (CHead e0 (Bind b0) u)
λb0:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b0) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C (CHead x1 (Bind b) x2) (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead x1 (Bind b) x2) (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b0) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
end of h1
(h2)
by (clear_gen_bind . . . . H13)
eq C e (CHead x1 (Bind b) x2)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or4
getl n c2 e
ex3_4
B
C
T
T
λb0:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b0) u)
λb0:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b0) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b0) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
∀H11:drop n O c2 (CHead x1 (Bind b) x3)
.∀H12:subst0 (minus i (s (Bind b) n)) v x2 x3
.∀H13:clear (CHead x1 (Bind b) x2) e
.or4
getl n c2 e
ex3_4
B
C
T
T
λb0:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b0) u)
λb0:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b0) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b0) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
assume f: F
suppose H11: drop n O c2 (CHead x1 (Flat f) x3)
suppose : subst0 (minus i (s (Flat f) n)) v x2 x3
suppose H13: clear (CHead x1 (Flat f) x2) e
by (clear_gen_flat . . . . H13)
we proved clear x1 e
by (clear_flat . . previous . .)
we proved clear (CHead x1 (Flat f) x3) e
by (getl_intro . . . . H11 previous)
we proved getl n c2 e
by (or4_intro0 . . . . previous)
we proved
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
∀H11:drop n O c2 (CHead x1 (Flat f) x3)
.subst0 (minus i (s (Flat f) n)) v x2 x3
→∀H13:clear (CHead x1 (Flat f) x2) e
.or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (previous . H8 H9 H10)
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case or4_intro2 : H6:ex3_4 K C C T λk:K.λe1:C.λ:C.λu:T.eq C x (CHead e1 k u) λk:K.λ:C.λe2:C.λu:T.drop n O c2 (CHead e2 k u) λk:K.λe1:C.λe2:C.λ:T.csubst0 (minus i (s k n)) v e1 e2 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proceed by induction on H6 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case ex3_4_intro : x0:K x1:C x2:C x3:T H7:eq C x (CHead x1 x0 x3) H8:drop n O c2 (CHead x2 x0 x3) H9:csubst0 (minus i (s x0 n)) v x1 x2 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
(H10)
we proceed by induction on H7 to prove clear (CHead x1 x0 x3) e
case refl_equal : ⇒
the thesis becomes the hypothesis H4
clear (CHead x1 x0 x3) e
end of H10
assume b: B
suppose H11: drop n O c2 (CHead x2 (Bind b) x3)
suppose H12: csubst0 (minus i (s (Bind b) n)) v x1 x2
suppose H13: clear (CHead x1 (Bind b) x3) e
(h1)
(h1)
by (refl_equal . .)
eq C (CHead x1 (Bind b) x3) (CHead x1 (Bind b) x3)
end of h1
(h2)
by (clear_bind . . .)
we proved clear (CHead x2 (Bind b) x3) (CHead x2 (Bind b) x3)
by (getl_intro . . . . H11 previous)
getl n c2 (CHead x2 (Bind b) x3)
end of h2
(h3)
consider H12
we proved csubst0 (minus i (s (Bind b) n)) v x1 x2
csubst0 (minus i (S n)) v x1 x2
end of h3
by (ex3_4_intro . . . . . . . . . . . h1 h2 h3)
we proved
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C (CHead x1 (Bind b) x3) (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
by (or4_intro2 . . . . previous)
or4
getl n c2 (CHead x1 (Bind b) x3)
ex3_4
B
C
T
T
λb0:B.λe0:C.λu:T.λ:T.eq C (CHead x1 (Bind b) x3) (CHead e0 (Bind b0) u)
λb0:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b0) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C (CHead x1 (Bind b) x3) (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead x1 (Bind b) x3) (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b0) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
end of h1
(h2)
by (clear_gen_bind . . . . H13)
eq C e (CHead x1 (Bind b) x3)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or4
getl n c2 e
ex3_4
B
C
T
T
λb0:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b0) u)
λb0:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b0) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b0) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
∀H11:drop n O c2 (CHead x2 (Bind b) x3)
.∀H12:csubst0 (minus i (s (Bind b) n)) v x1 x2
.∀H13:clear (CHead x1 (Bind b) x3) e
.or4
getl n c2 e
ex3_4
B
C
T
T
λb0:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b0) u)
λb0:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b0) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b0) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
assume f: F
suppose H11: drop n O c2 (CHead x2 (Flat f) x3)
suppose H12: csubst0 (minus i (s (Flat f) n)) v x1 x2
suppose H13: clear (CHead x1 (Flat f) x3) e
(H14)
by (minus_x_Sy . . H)
we proved eq nat (minus i n) (S (minus i (S n)))
we proceed by induction on the previous result to prove csubst0 (S (minus i (S n))) v x1 x2
case refl_equal : ⇒
the thesis becomes csubst0 (minus i n) v x1 x2
consider H12
we proved csubst0 (minus i (s (Flat f) n)) v x1 x2
csubst0 (minus i n) v x1 x2
csubst0 (S (minus i (S n))) v x1 x2
end of H14
(H15)
by (clear_gen_flat . . . . H13)
we proved clear x1 e
by (csubst0_clear_S . . . . H14 . previous)
or4
clear x2 e
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C e (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear x2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 (minus i (S n)) v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear x2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C e (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear x2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 (minus i (S n)) v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
end of H15
we proceed by induction on H15 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case or4_intro0 : H16:clear x2 e ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (clear_flat . . H16 . .)
we proved clear (CHead x2 (Flat f) x3) e
by (getl_intro . . . . H11 previous)
we proved getl n c2 e
by (or4_intro0 . . . . previous)
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case or4_intro1 : H16:ex3_4 B C T T λb:B.λe0:C.λu1:T.λ:T.eq C e (CHead e0 (Bind b) u1) λb:B.λe0:C.λ:T.λu2:T.clear x2 (CHead e0 (Bind b) u2) λ:B.λ:C.λu1:T.λu2:T.subst0 (minus i (S n)) v u1 u2 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proceed by induction on H16 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case ex3_4_intro : x4:B x5:C x6:T x7:T H17:eq C e (CHead x5 (Bind x4) x6) H18:clear x2 (CHead x5 (Bind x4) x7) H19:subst0 (minus i (S n)) v x6 x7 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
(h1)
by (refl_equal . .)
eq C (CHead x5 (Bind x4) x6) (CHead x5 (Bind x4) x6)
end of h1
(h2)
by (clear_flat . . H18 . .)
we proved clear (CHead x2 (Flat f) x3) (CHead x5 (Bind x4) x7)
by (getl_intro . . . . H11 previous)
getl n c2 (CHead x5 (Bind x4) x7)
end of h2
by (ex3_4_intro . . . . . . . . . . . h1 h2 H19)
we proved
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C (CHead x5 (Bind x4) x6) (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
by (or4_intro1 . . . . previous)
we proved
or4
getl n c2 (CHead x5 (Bind x4) x6)
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C (CHead x5 (Bind x4) x6) (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C (CHead x5 (Bind x4) x6) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead x5 (Bind x4) x6) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (eq_ind_r . . . previous . H17)
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case or4_intro2 : H16:ex3_4 B C C T λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u) λb:B.λ:C.λe2:C.λu:T.clear x2 (CHead e2 (Bind b) u) λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proceed by induction on H16 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case ex3_4_intro : x4:B x5:C x6:C x7:T H17:eq C e (CHead x5 (Bind x4) x7) H18:clear x2 (CHead x6 (Bind x4) x7) H19:csubst0 (minus i (S n)) v x5 x6 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
(h1)
by (refl_equal . .)
eq C (CHead x5 (Bind x4) x7) (CHead x5 (Bind x4) x7)
end of h1
(h2)
by (clear_flat . . H18 . .)
we proved clear (CHead x2 (Flat f) x3) (CHead x6 (Bind x4) x7)
by (getl_intro . . . . H11 previous)
getl n c2 (CHead x6 (Bind x4) x7)
end of h2
by (ex3_4_intro . . . . . . . . . . . h1 h2 H19)
we proved
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C (CHead x5 (Bind x4) x7) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
by (or4_intro2 . . . . previous)
we proved
or4
getl n c2 (CHead x5 (Bind x4) x7)
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C (CHead x5 (Bind x4) x7) (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C (CHead x5 (Bind x4) x7) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead x5 (Bind x4) x7) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (eq_ind_r . . . previous . H17)
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case or4_intro3 : H16:ex4_5 B C C T T λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C e (CHead e1 (Bind b) u1) λb:B.λ:C.λe2:C.λ:T.λu2:T.clear x2 (CHead e2 (Bind b) u2) λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 (minus i (S n)) v u1 u2 λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proceed by induction on H16 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case ex4_5_intro : x4:B x5:C x6:C x7:T x8:T H17:eq C e (CHead x5 (Bind x4) x7) H18:clear x2 (CHead x6 (Bind x4) x8) H19:subst0 (minus i (S n)) v x7 x8 H20:csubst0 (minus i (S n)) v x5 x6 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
(h1)
by (refl_equal . .)
eq C (CHead x5 (Bind x4) x7) (CHead x5 (Bind x4) x7)
end of h1
(h2)
by (clear_flat . . H18 . .)
we proved clear (CHead x2 (Flat f) x3) (CHead x6 (Bind x4) x8)
by (getl_intro . . . . H11 previous)
getl n c2 (CHead x6 (Bind x4) x8)
end of h2
by (ex4_5_intro . . . . . . . . . . . . . . h1 h2 H19 H20)
we proved
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead x5 (Bind x4) x7) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (or4_intro3 . . . . previous)
we proved
or4
getl n c2 (CHead x5 (Bind x4) x7)
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C (CHead x5 (Bind x4) x7) (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C (CHead x5 (Bind x4) x7) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead x5 (Bind x4) x7) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (eq_ind_r . . . previous . H17)
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proved
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
∀H11:drop n O c2 (CHead x2 (Flat f) x3)
.∀H12:csubst0 (minus i (s (Flat f) n)) v x1 x2
.∀H13:clear (CHead x1 (Flat f) x3) e
.or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (previous . H8 H9 H10)
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case or4_intro3 : H6:ex4_5 K C C T T λk:K.λe1:C.λ:C.λu:T.λ:T.eq C x (CHead e1 k u) λk:K.λ:C.λe2:C.λ:T.λw:T.drop n O c2 (CHead e2 k w) λk:K.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (s k n)) v u w λk:K.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (s k n)) v e1 e2 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proceed by induction on H6 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case ex4_5_intro : x0:K x1:C x2:C x3:T x4:T H7:eq C x (CHead x1 x0 x3) H8:drop n O c2 (CHead x2 x0 x4) H9:subst0 (minus i (s x0 n)) v x3 x4 H10:csubst0 (minus i (s x0 n)) v x1 x2 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
(H11)
we proceed by induction on H7 to prove clear (CHead x1 x0 x3) e
case refl_equal : ⇒
the thesis becomes the hypothesis H4
clear (CHead x1 x0 x3) e
end of H11
assume b: B
suppose H12: drop n O c2 (CHead x2 (Bind b) x4)
suppose H13: subst0 (minus i (s (Bind b) n)) v x3 x4
suppose H14: csubst0 (minus i (s (Bind b) n)) v x1 x2
suppose H15: clear (CHead x1 (Bind b) x3) e
(h1)
(h1)
by (refl_equal . .)
eq C (CHead x1 (Bind b) x3) (CHead x1 (Bind b) x3)
end of h1
(h2)
by (clear_bind . . .)
we proved clear (CHead x2 (Bind b) x4) (CHead x2 (Bind b) x4)
by (getl_intro . . . . H12 previous)
getl n c2 (CHead x2 (Bind b) x4)
end of h2
(h3)
consider H13
we proved subst0 (minus i (s (Bind b) n)) v x3 x4
subst0 (minus i (S n)) v x3 x4
end of h3
(h4)
consider H14
we proved csubst0 (minus i (s (Bind b) n)) v x1 x2
csubst0 (minus i (S n)) v x1 x2
end of h4
by (ex4_5_intro . . . . . . . . . . . . . . h1 h2 h3 h4)
we proved
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead x1 (Bind b) x3) (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b0) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (or4_intro3 . . . . previous)
or4
getl n c2 (CHead x1 (Bind b) x3)
ex3_4
B
C
T
T
λb0:B.λe0:C.λu:T.λ:T.eq C (CHead x1 (Bind b) x3) (CHead e0 (Bind b0) u)
λb0:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b0) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C (CHead x1 (Bind b) x3) (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead x1 (Bind b) x3) (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b0) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
end of h1
(h2)
by (clear_gen_bind . . . . H15)
eq C e (CHead x1 (Bind b) x3)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or4
getl n c2 e
ex3_4
B
C
T
T
λb0:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b0) u)
λb0:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b0) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b0) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
∀H12:drop n O c2 (CHead x2 (Bind b) x4)
.∀H13:subst0 (minus i (s (Bind b) n)) v x3 x4
.∀H14:csubst0 (minus i (s (Bind b) n)) v x1 x2
.∀H15:clear (CHead x1 (Bind b) x3) e
.or4
getl n c2 e
ex3_4
B
C
T
T
λb0:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b0) u)
λb0:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b0) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb0:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b0) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb0:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b0) u)
λb0:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b0) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
assume f: F
suppose H12: drop n O c2 (CHead x2 (Flat f) x4)
suppose : subst0 (minus i (s (Flat f) n)) v x3 x4
suppose H14: csubst0 (minus i (s (Flat f) n)) v x1 x2
suppose H15: clear (CHead x1 (Flat f) x3) e
(H16)
by (minus_x_Sy . . H)
we proved eq nat (minus i n) (S (minus i (S n)))
we proceed by induction on the previous result to prove csubst0 (S (minus i (S n))) v x1 x2
case refl_equal : ⇒
the thesis becomes csubst0 (minus i n) v x1 x2
consider H14
we proved csubst0 (minus i (s (Flat f) n)) v x1 x2
csubst0 (minus i n) v x1 x2
csubst0 (S (minus i (S n))) v x1 x2
end of H16
(H17)
by (clear_gen_flat . . . . H15)
we proved clear x1 e
by (csubst0_clear_S . . . . H16 . previous)
or4
clear x2 e
ex3_4
B
C
T
T
λb:B.λe:C.λu1:T.λ:T.eq C e (CHead e (Bind b) u1)
λb:B.λe:C.λ:T.λu2:T.clear x2 (CHead e (Bind b) u2)
λ:B.λ:C.λu1:T.λu2:T.subst0 (minus i (S n)) v u1 u2
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.clear x2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C e (CHead e1 (Bind b) u1)
λb:B.λ:C.λe2:C.λ:T.λu2:T.clear x2 (CHead e2 (Bind b) u2)
λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 (minus i (S n)) v u1 u2
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
end of H17
we proceed by induction on H17 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case or4_intro0 : H18:clear x2 e ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (clear_flat . . H18 . .)
we proved clear (CHead x2 (Flat f) x4) e
by (getl_intro . . . . H12 previous)
we proved getl n c2 e
by (or4_intro0 . . . . previous)
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case or4_intro1 : H18:ex3_4 B C T T λb:B.λe0:C.λu1:T.λ:T.eq C e (CHead e0 (Bind b) u1) λb:B.λe0:C.λ:T.λu2:T.clear x2 (CHead e0 (Bind b) u2) λ:B.λ:C.λu1:T.λu2:T.subst0 (minus i (S n)) v u1 u2 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proceed by induction on H18 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case ex3_4_intro : x5:B x6:C x7:T x8:T H19:eq C e (CHead x6 (Bind x5) x7) H20:clear x2 (CHead x6 (Bind x5) x8) H21:subst0 (minus i (S n)) v x7 x8 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
(h1)
by (refl_equal . .)
eq C (CHead x6 (Bind x5) x7) (CHead x6 (Bind x5) x7)
end of h1
(h2)
by (clear_flat . . H20 . .)
we proved clear (CHead x2 (Flat f) x4) (CHead x6 (Bind x5) x8)
by (getl_intro . . . . H12 previous)
getl n c2 (CHead x6 (Bind x5) x8)
end of h2
by (ex3_4_intro . . . . . . . . . . . h1 h2 H21)
we proved
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C (CHead x6 (Bind x5) x7) (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
by (or4_intro1 . . . . previous)
we proved
or4
getl n c2 (CHead x6 (Bind x5) x7)
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C (CHead x6 (Bind x5) x7) (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C (CHead x6 (Bind x5) x7) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead x6 (Bind x5) x7) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (eq_ind_r . . . previous . H19)
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case or4_intro2 : H18:ex3_4 B C C T λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u) λb:B.λ:C.λe2:C.λu:T.clear x2 (CHead e2 (Bind b) u) λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proceed by induction on H18 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case ex3_4_intro : x5:B x6:C x7:C x8:T H19:eq C e (CHead x6 (Bind x5) x8) H20:clear x2 (CHead x7 (Bind x5) x8) H21:csubst0 (minus i (S n)) v x6 x7 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
(h1)
by (refl_equal . .)
eq C (CHead x6 (Bind x5) x8) (CHead x6 (Bind x5) x8)
end of h1
(h2)
by (clear_flat . . H20 . .)
we proved clear (CHead x2 (Flat f) x4) (CHead x7 (Bind x5) x8)
by (getl_intro . . . . H12 previous)
getl n c2 (CHead x7 (Bind x5) x8)
end of h2
by (ex3_4_intro . . . . . . . . . . . h1 h2 H21)
we proved
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C (CHead x6 (Bind x5) x8) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
by (or4_intro2 . . . . previous)
we proved
or4
getl n c2 (CHead x6 (Bind x5) x8)
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C (CHead x6 (Bind x5) x8) (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C (CHead x6 (Bind x5) x8) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead x6 (Bind x5) x8) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (eq_ind_r . . . previous . H19)
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case or4_intro3 : H18:ex4_5 B C C T T λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C e (CHead e1 (Bind b) u1) λb:B.λ:C.λe2:C.λ:T.λu2:T.clear x2 (CHead e2 (Bind b) u2) λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 (minus i (S n)) v u1 u2 λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proceed by induction on H18 to prove
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
case ex4_5_intro : x5:B x6:C x7:C x8:T x9:T H19:eq C e (CHead x6 (Bind x5) x8) H20:clear x2 (CHead x7 (Bind x5) x9) H21:subst0 (minus i (S n)) v x8 x9 H22:csubst0 (minus i (S n)) v x6 x7 ⇒
the thesis becomes
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
(h1)
by (refl_equal . .)
eq C (CHead x6 (Bind x5) x8) (CHead x6 (Bind x5) x8)
end of h1
(h2)
by (clear_flat . . H20 . .)
we proved clear (CHead x2 (Flat f) x4) (CHead x7 (Bind x5) x9)
by (getl_intro . . . . H12 previous)
getl n c2 (CHead x7 (Bind x5) x9)
end of h2
by (ex4_5_intro . . . . . . . . . . . . . . h1 h2 H21 H22)
we proved
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead x6 (Bind x5) x8) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (or4_intro3 . . . . previous)
we proved
or4
getl n c2 (CHead x6 (Bind x5) x8)
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C (CHead x6 (Bind x5) x8) (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C (CHead x6 (Bind x5) x8) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C (CHead x6 (Bind x5) x8) (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (eq_ind_r . . . previous . H19)
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proved
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
∀H12:drop n O c2 (CHead x2 (Flat f) x4)
.subst0 (minus i (s (Flat f) n)) v x3 x4
→∀H14:csubst0 (minus i (s (Flat f) n)) v x1 x2
.∀H15:clear (CHead x1 (Flat f) x3) e
.or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
by (previous . H8 H9 H10 H11)
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proved
or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2
we proved
∀i:nat
.∀n:nat
.lt n i
→∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e:C
.getl n c1 e
→(or4
getl n c2 e
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
ex3_4
B
C
C
T
λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
ex4_5
B
C
C
T
T
λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2)