DEFINITION csubst0_getl_lt_back()
TYPE =
∀n:nat
.∀i:nat
.lt n i
→∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C.(getl n c2 e2)→(or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1))
BODY =
assume n: nat
assume i: nat
suppose H: lt n i
assume c1: C
assume c2: C
assume v: T
suppose H0: csubst0 i v c1 c2
assume e2: C
suppose H1: getl n c2 e2
(H2)
by (getl_gen_all . . . H1)
ex2 C λe:C.drop n O c2 e λe:C.clear e e2
end of H2
we proceed by induction on H2 to prove or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
case ex_intro2 : x:C H3:drop n O c2 x H4:clear x e2 ⇒
the thesis becomes or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
(H_x)
by (csubst0_drop_lt_back . . H . . . H0 . H3)
or (drop n O c1 x) (ex2 C λe1:C.csubst0 (minus i n) v e1 x λe1:C.drop n O c1 e1)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
case or_introl : H6:drop n O c1 x ⇒
the thesis becomes or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
by (getl_intro . . . . H6 H4)
we proved getl n c1 e2
by (or_introl . . previous)
or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
case or_intror : H6:ex2 C λe1:C.csubst0 (minus i n) v e1 x λe1:C.drop n O c1 e1 ⇒
the thesis becomes or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
we proceed by induction on H6 to prove or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
case ex_intro2 : x0:C H7:csubst0 (minus i n) v x0 x H8:drop n O c1 x0 ⇒
the thesis becomes or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
(H_x0)
by (csubst0_clear_trans . . . . H7 . H4)
or (clear x0 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.clear x0 e1)
end of H_x0
(H9) consider H_x0
we proceed by induction on H9 to prove or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
case or_introl : H10:clear x0 e2 ⇒
the thesis becomes or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
by (getl_intro . . . . H8 H10)
we proved getl n c1 e2
by (or_introl . . previous)
or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
case or_intror : H10:ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.clear x0 e1 ⇒
the thesis becomes or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
we proceed by induction on H10 to prove or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
case ex_intro2 : x1:C H11:csubst0 (minus i n) v x1 e2 H12:clear x0 x1 ⇒
the thesis becomes or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
by (getl_intro . . . . H8 H12)
we proved getl n c1 x1
by (ex_intro2 . . . . H11 previous)
we proved ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1
by (or_intror . . previous)
or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
we proved or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1)
we proved
∀n:nat
.∀i:nat
.lt n i
→∀c1:C
.∀c2:C
.∀v:T
.csubst0 i v c1 c2
→∀e2:C.(getl n c2 e2)→(or (getl n c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.getl n c1 e1))