DEFINITION csubst0_getl_ge()
TYPE =
∀i:nat
.∀n:nat.(le i n)→∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(getl n c1 e)→(getl n c2 e)
BODY =
assume i: nat
assume n: nat
suppose H: le i n
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 getl n c2 e
case ex_intro2 : x:C H3:drop n O c1 x H4:clear x e ⇒
the thesis becomes getl n c2 e
(h1)
suppose H5: lt i n
by (csubst0_drop_gt . . H5 . . . H0 . H3)
we proved drop n O c2 x
by (getl_intro . . . . previous H4)
we proved getl n c2 e
(lt i n)→(getl n c2 e)
end of h1
(h2)
suppose H5: eq nat i n
(H6)
by (eq_ind_r . . . H3 . H5)
drop i O c1 x
end of H6
we proceed by induction on H5 to prove getl n c2 e
case refl_equal : ⇒
the thesis becomes getl i c2 e
(H8)
by (csubst0_drop_eq . . . . H0 . H6)
or4
drop i O c2 x
ex3_4
F
C
T
T
λf:F.λe0:C.λu:T.λ:T.eq C x (CHead e0 (Flat f) u)
λf:F.λe0:C.λ:T.λw:T.drop i O c2 (CHead e0 (Flat f) w)
λ:F.λ:C.λu:T.λw:T.subst0 O v u w
ex3_4
F
C
C
T
λf:F.λe1:C.λ:C.λu:T.eq C x (CHead e1 (Flat f) u)
λf:F.λ:C.λe2:C.λu:T.drop i O c2 (CHead e2 (Flat f) u)
λ:F.λe1:C.λe2:C.λ:T.csubst0 O v e1 e2
ex4_5
F
C
C
T
T
λf:F.λe1:C.λ:C.λu:T.λ:T.eq C x (CHead e1 (Flat f) u)
λf:F.λ:C.λe2:C.λ:T.λw:T.drop i O c2 (CHead e2 (Flat f) w)
λ:F.λ:C.λ:C.λu:T.λw:T.subst0 O v u w
λ:F.λe1:C.λe2:C.λ:T.λ:T.csubst0 O v e1 e2
end of H8
we proceed by induction on H8 to prove getl i c2 e
case or4_intro0 : H9:drop i O c2 x ⇒
the thesis becomes getl i c2 e
by (getl_intro . . . . H9 H4)
getl i c2 e
case or4_intro1 : H9:ex3_4 F C T T λf:F.λe0:C.λu:T.λ:T.eq C x (CHead e0 (Flat f) u) λf:F.λe0:C.λ:T.λw:T.drop i O c2 (CHead e0 (Flat f) w) λ:F.λ:C.λu:T.λw:T.subst0 O v u w ⇒
the thesis becomes getl i c2 e
we proceed by induction on H9 to prove getl i c2 e
case ex3_4_intro : x0:F x1:C x2:T x3:T H10:eq C x (CHead x1 (Flat x0) x2) H11:drop i O c2 (CHead x1 (Flat x0) x3) :subst0 O v x2 x3 ⇒
the thesis becomes getl i c2 e
(H13)
we proceed by induction on H10 to prove clear (CHead x1 (Flat x0) x2) e
case refl_equal : ⇒
the thesis becomes the hypothesis H4
clear (CHead x1 (Flat x0) x2) e
end of H13
by (clear_gen_flat . . . . H13)
we proved clear x1 e
by (clear_flat . . previous . .)
we proved clear (CHead x1 (Flat x0) x3) e
by (getl_intro . . . . H11 previous)
getl i c2 e
getl i c2 e
case or4_intro2 : H9:ex3_4 F C C T λf:F.λe1:C.λ:C.λu:T.eq C x (CHead e1 (Flat f) u) λf:F.λ:C.λe2:C.λu:T.drop i O c2 (CHead e2 (Flat f) u) λ:F.λe1:C.λe2:C.λ:T.csubst0 O v e1 e2 ⇒
the thesis becomes getl i c2 e
we proceed by induction on H9 to prove getl i c2 e
case ex3_4_intro : x0:F x1:C x2:C x3:T H10:eq C x (CHead x1 (Flat x0) x3) H11:drop i O c2 (CHead x2 (Flat x0) x3) H12:csubst0 O v x1 x2 ⇒
the thesis becomes getl i c2 e
(H13)
we proceed by induction on H10 to prove clear (CHead x1 (Flat x0) x3) e
case refl_equal : ⇒
the thesis becomes the hypothesis H4
clear (CHead x1 (Flat x0) x3) e
end of H13
by (clear_gen_flat . . . . H13)
we proved clear x1 e
by (csubst0_clear_O . . . H12 . previous)
we proved clear x2 e
by (clear_flat . . previous . .)
we proved clear (CHead x2 (Flat x0) x3) e
by (getl_intro . . . . H11 previous)
getl i c2 e
getl i c2 e
case or4_intro3 : H9:ex4_5 F C C T T λf:F.λe1:C.λ:C.λu:T.λ:T.eq C x (CHead e1 (Flat f) u) λf:F.λ:C.λe2:C.λ:T.λw:T.drop i O c2 (CHead e2 (Flat f) w) λ:F.λ:C.λ:C.λu:T.λw:T.subst0 O v u w λ:F.λe1:C.λe2:C.λ:T.λ:T.csubst0 O v e1 e2 ⇒
the thesis becomes getl i c2 e
we proceed by induction on H9 to prove getl i c2 e
case ex4_5_intro : x0:F x1:C x2:C x3:T x4:T H10:eq C x (CHead x1 (Flat x0) x3) H11:drop i O c2 (CHead x2 (Flat x0) x4) :subst0 O v x3 x4 H13:csubst0 O v x1 x2 ⇒
the thesis becomes getl i c2 e
(H14)
we proceed by induction on H10 to prove clear (CHead x1 (Flat x0) x3) e
case refl_equal : ⇒
the thesis becomes the hypothesis H4
clear (CHead x1 (Flat x0) x3) e
end of H14
by (clear_gen_flat . . . . H14)
we proved clear x1 e
by (csubst0_clear_O . . . H13 . previous)
we proved clear x2 e
by (clear_flat . . previous . .)
we proved clear (CHead x2 (Flat x0) x4) e
by (getl_intro . . . . H11 previous)
getl i c2 e
getl i c2 e
getl i c2 e
we proved getl n c2 e
(eq nat i n)→(getl n c2 e)
end of h2
(h3)
suppose H5: lt n i
by (le_lt_false . . H H5 .)
we proved getl n c2 e
(lt n i)→(getl n c2 e)
end of h3
by (lt_eq_gt_e . . . h1 h2 h3)
getl n c2 e
we proved getl n c2 e
we proved
∀i:nat
.∀n:nat.(le i n)→∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(getl n c1 e)→(getl n c2 e)