DEFINITION csubst1_getl_lt()
TYPE =
∀i:nat
.∀n:nat
.lt n i
→∀c1:C
.∀c2:C.∀v:T.(csubst1 i v c1 c2)→∀e1:C.(getl n c1 e1)→(ex2 C λe2:C.csubst1 (minus i n) v e1 e2 λe2:C.getl n c2 e2)
BODY =
assume i: nat
assume n: nat
suppose H: lt n i
assume c1: C
assume c2: C
assume v: T
suppose H0: csubst1 i v c1 c2
we proceed by induction on H0 to prove ∀e1:C.(getl n c1 e1)→(ex2 C λe2:C.csubst1 (minus i n) v e1 e2 λe2:C.getl n c2 e2)
case csubst1_refl : ⇒
the thesis becomes ∀e1:C.(getl n c1 e1)→(ex2 C λe2:C.csubst1 (minus i n) v e1 e2 λe2:C.getl n c1 e2)
assume e1: C
suppose H1: getl n c1 e1
(h1)
by (csubst1_refl . . .)
we proved csubst1 (S (minus i (S n))) v e1 e1
by (ex_intro2 . . . . previous H1)
ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c1 e2
end of h1
(h2)
by (minus_x_Sy . . H)
eq nat (minus i n) (S (minus i (S n)))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 C λe2:C.csubst1 (minus i n) v e1 e2 λe2:C.getl n c1 e2
∀e1:C.(getl n c1 e1)→(ex2 C λe2:C.csubst1 (minus i n) v e1 e2 λe2:C.getl n c1 e2)
case csubst1_sing : c3:C H1:csubst0 i v c1 c3 ⇒
the thesis becomes ∀e1:C.∀H2:(getl n c1 e1).(ex2 C λe2:C.csubst1 (minus i n) v e1 e2 λe2:C.getl n c3 e2)
assume e1: C
suppose H2: getl n c1 e1
(h1)
(H3)
by (csubst0_getl_lt . . H . . . H1 . H2)
or4
getl n c3 e1
ex3_4
B
C
T
T
λb:B.λe0:C.λu:T.λ:T.eq C e1 (CHead e0 (Bind b) u)
λb:B.λe0:C.λ:T.λw:T.getl n c3 (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 e1 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λu:T.getl n c3 (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 e1 (CHead e1 (Bind b) u)
λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c3 (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
end of H3
we proceed by induction on H3 to prove ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
case or4_intro0 : H4:getl n c3 e1 ⇒
the thesis becomes ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
by (csubst1_refl . . .)
we proved csubst1 (S (minus i (S n))) v e1 e1
by (ex_intro2 . . . . previous H4)
ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
case or4_intro1 : H4:ex3_4 B C T T λb:B.λe0:C.λu:T.λ:T.eq C e1 (CHead e0 (Bind b) u) λb:B.λe0:C.λ:T.λw:T.getl n c3 (CHead e0 (Bind b) w) λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w ⇒
the thesis becomes ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
we proceed by induction on H4 to prove ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
case ex3_4_intro : x0:B x1:C x2:T x3:T H5:eq C e1 (CHead x1 (Bind x0) x2) H6:getl n c3 (CHead x1 (Bind x0) x3) H7:subst0 (minus i (S n)) v x2 x3 ⇒
the thesis becomes ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
by (csubst0_snd_bind . . . . . H7 .)
we proved csubst0 (S (minus i (S n))) v (CHead x1 (Bind x0) x2) (CHead x1 (Bind x0) x3)
by (csubst1_sing . . . . previous)
we proved csubst1 (S (minus i (S n))) v (CHead x1 (Bind x0) x2) (CHead x1 (Bind x0) x3)
by (ex_intro2 . . . . previous H6)
we proved ex2 C λe2:C.csubst1 (S (minus i (S n))) v (CHead x1 (Bind x0) x2) e2 λe2:C.getl n c3 e2
by (eq_ind_r . . . previous . H5)
ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
case or4_intro2 : H4:ex3_4 B C C T λb:B.λe2:C.λ:C.λu:T.eq C e1 (CHead e2 (Bind b) u) λb:B.λ:C.λe3:C.λu:T.getl n c3 (CHead e3 (Bind b) u) λ:B.λe2:C.λe3:C.λ:T.csubst0 (minus i (S n)) v e2 e3 ⇒
the thesis becomes ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
we proceed by induction on H4 to prove ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
case ex3_4_intro : x0:B x1:C x2:C x3:T H5:eq C e1 (CHead x1 (Bind x0) x3) H6:getl n c3 (CHead x2 (Bind x0) x3) H7:csubst0 (minus i (S n)) v x1 x2 ⇒
the thesis becomes ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
by (csubst0_fst_bind . . . . . H7 .)
we proved csubst0 (S (minus i (S n))) v (CHead x1 (Bind x0) x3) (CHead x2 (Bind x0) x3)
by (csubst1_sing . . . . previous)
we proved csubst1 (S (minus i (S n))) v (CHead x1 (Bind x0) x3) (CHead x2 (Bind x0) x3)
by (ex_intro2 . . . . previous H6)
we proved ex2 C λe2:C.csubst1 (S (minus i (S n))) v (CHead x1 (Bind x0) x3) e2 λe2:C.getl n c3 e2
by (eq_ind_r . . . previous . H5)
ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
case or4_intro3 : H4:ex4_5 B C C T T λb:B.λe2:C.λ:C.λu:T.λ:T.eq C e1 (CHead e2 (Bind b) u) λb:B.λ:C.λe3:C.λ:T.λw:T.getl n c3 (CHead e3 (Bind b) w) λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w λ:B.λe2:C.λe3:C.λ:T.λ:T.csubst0 (minus i (S n)) v e2 e3 ⇒
the thesis becomes ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
we proceed by induction on H4 to prove ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
case ex4_5_intro : x0:B x1:C x2:C x3:T x4:T H5:eq C e1 (CHead x1 (Bind x0) x3) H6:getl n c3 (CHead x2 (Bind x0) x4) H7:subst0 (minus i (S n)) v x3 x4 H8:csubst0 (minus i (S n)) v x1 x2 ⇒
the thesis becomes ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
by (csubst0_both_bind . . . . . H7 . . H8)
we proved csubst0 (S (minus i (S n))) v (CHead x1 (Bind x0) x3) (CHead x2 (Bind x0) x4)
by (csubst1_sing . . . . previous)
we proved csubst1 (S (minus i (S n))) v (CHead x1 (Bind x0) x3) (CHead x2 (Bind x0) x4)
by (ex_intro2 . . . . previous H6)
we proved ex2 C λe2:C.csubst1 (S (minus i (S n))) v (CHead x1 (Bind x0) x3) e2 λe2:C.getl n c3 e2
by (eq_ind_r . . . previous . H5)
ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
ex2 C λe2:C.csubst1 (S (minus i (S n))) v e1 e2 λe2:C.getl n c3 e2
end of h1
(h2)
by (minus_x_Sy . . H)
eq nat (minus i n) (S (minus i (S n)))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 C λe2:C.csubst1 (minus i n) v e1 e2 λe2:C.getl n c3 e2
∀e1:C.∀H2:(getl n c1 e1).(ex2 C λe2:C.csubst1 (minus i n) v e1 e2 λe2:C.getl n c3 e2)
we proved ∀e1:C.(getl n c1 e1)→(ex2 C λe2:C.csubst1 (minus i n) v e1 e2 λe2:C.getl n c2 e2)
we proved
∀i:nat
.∀n:nat
.lt n i
→∀c1:C
.∀c2:C.∀v:T.(csubst1 i v c1 c2)→∀e1:C.(getl n c1 e1)→(ex2 C λe2:C.csubst1 (minus i n) v e1 e2 λe2:C.getl n c2 e2)