DEFINITION pr2_gen_lift()
TYPE =
∀c:C
.∀t1:T
.∀x:T
.∀h:nat
.∀d:nat
.pr2 c (lift h d t1) x
→∀e:C.(drop h d c e)→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr2 e t1 t2)
BODY =
assume c: C
assume t1: T
assume x: T
assume h: nat
assume d: nat
suppose H: pr2 c (lift h d t1) x
assume y: T
suppose H0: pr2 c y x
we proceed by induction on H0 to prove
eq T y (lift h d t1)
→∀e:C.(drop h d c e)→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr2 e t1 t2)
case pr2_free : c0:C t0:T t2:T H1:pr0 t0 t2 ⇒
the thesis becomes
∀H2:eq T t0 (lift h d t1)
.∀e:C.(drop h d c0 e)→(ex2 T λt3:T.eq T t2 (lift h d t3) λt3:T.pr2 e t1 t3)
suppose H2: eq T t0 (lift h d t1)
assume e: C
suppose : drop h d c0 e
(H4)
we proceed by induction on H2 to prove pr0 (lift h d t1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
pr0 (lift h d t1) t2
end of H4
by (pr0_gen_lift . . . . H4)
we proved ex2 T λt2:T.eq T t2 (lift h d t2) λt2:T.pr0 t1 t2
we proceed by induction on the previous result to prove ex2 T λt3:T.eq T t2 (lift h d t3) λt3:T.pr2 e t1 t3
case ex_intro2 : x0:T H5:eq T t2 (lift h d x0) H6:pr0 t1 x0 ⇒
the thesis becomes ex2 T λt3:T.eq T t2 (lift h d t3) λt3:T.pr2 e t1 t3
(h1)
by (refl_equal . .)
eq T (lift h d x0) (lift h d x0)
end of h1
(h2)
by (pr2_free . . . H6)
pr2 e t1 x0
end of h2
by (ex_intro2 . . . . h1 h2)
we proved ex2 T λt3:T.eq T (lift h d x0) (lift h d t3) λt3:T.pr2 e t1 t3
by (eq_ind_r . . . previous . H5)
ex2 T λt3:T.eq T t2 (lift h d t3) λt3:T.pr2 e t1 t3
we proved ex2 T λt3:T.eq T t2 (lift h d t3) λt3:T.pr2 e t1 t3
∀H2:eq T t0 (lift h d t1)
.∀e:C.(drop h d c0 e)→(ex2 T λt3:T.eq T t2 (lift h d t3) λt3:T.pr2 e t1 t3)
case pr2_delta : c0:C d0:C u:T i:nat H1:getl i c0 (CHead d0 (Bind Abbr) u) t0:T t2:T H2:pr0 t0 t2 t:T H3:subst0 i u t2 t ⇒
the thesis becomes ∀H4:(eq T t0 (lift h d t1)).∀e:C.∀H5:(drop h d c0 e).(ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3)
suppose H4: eq T t0 (lift h d t1)
assume e: C
suppose H5: drop h d c0 e
(H6)
we proceed by induction on H4 to prove pr0 (lift h d t1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
pr0 (lift h d t1) t2
end of H6
by (pr0_gen_lift . . . . H6)
we proved ex2 T λt2:T.eq T t2 (lift h d t2) λt2:T.pr0 t1 t2
we proceed by induction on the previous result to prove ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
case ex_intro2 : x0:T H7:eq T t2 (lift h d x0) H8:pr0 t1 x0 ⇒
the thesis becomes ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
(H9)
we proceed by induction on H7 to prove subst0 i u (lift h d x0) t
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 i u (lift h d x0) t
end of H9
(h1)
suppose H10: lt i d
(H11)
by (lt_plus_minus . . H10)
we proved eq nat d (S (plus i (minus d (S i))))
we proceed by induction on the previous result to prove subst0 i u (lift h (S (plus i (minus d (S i)))) x0) t
case refl_equal : ⇒
the thesis becomes the hypothesis H9
subst0 i u (lift h (S (plus i (minus d (S i)))) x0) t
end of H11
(H12)
by (lt_plus_minus . . H10)
we proved eq nat d (S (plus i (minus d (S i))))
we proceed by induction on the previous result to prove drop h (S (plus i (minus d (S i)))) c0 e
case refl_equal : ⇒
the thesis becomes the hypothesis H5
drop h (S (plus i (minus d (S i)))) c0 e
end of H12
by (getl_drop_conf_lt . . . . . H1 . . . H12)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (minus d (S i)) v)
λv:T.λe0:C.getl i e (CHead e0 (Bind Abbr) v)
λ:T.λe0:C.drop h (minus d (S i)) d0 e0
we proceed by induction on the previous result to prove ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
case ex3_2_intro : x1:T x2:C H13:eq T u (lift h (minus d (S i)) x1) H14:getl i e (CHead x2 (Bind Abbr) x1) :drop h (minus d (S i)) d0 x2 ⇒
the thesis becomes ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
(H16)
we proceed by induction on H13 to prove
subst0
i
lift h (minus d (S i)) x1
lift h (S (plus i (minus d (S i)))) x0
t
case refl_equal : ⇒
the thesis becomes the hypothesis H11
subst0
i
lift h (minus d (S i)) x1
lift h (S (plus i (minus d (S i)))) x0
t
end of H16
by (subst0_gen_lift_lt . . . . . . H16)
we proved ex2 T λt2:T.eq T t (lift h (S (plus i (minus d (S i)))) t2) λt2:T.subst0 i x1 x0 t2
we proceed by induction on the previous result to prove ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
case ex_intro2 : x3:T H17:eq T t (lift h (S (plus i (minus d (S i)))) x3) H18:subst0 i x1 x0 x3 ⇒
the thesis becomes ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
(H19)
by (lt_plus_minus . . H10)
we proved eq nat d (S (plus i (minus d (S i))))
by (eq_ind_r . . . H17 . previous)
eq T t (lift h d x3)
end of H19
by (pr2_delta . . . . H14 . . H8 . H18)
we proved pr2 e t1 x3
by (ex_intro2 . . . . H19 previous)
ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
we proved ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
(lt i d)→(ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3)
end of h1
(h2)
suppose H10: le d i
(h1)
suppose H11: lt i (plus d h)
by (subst0_gen_lift_false . . . . . . H10 H11 H9 .)
we proved ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
(lt i (plus d h))→(ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3)
end of h1
(h2)
suppose H11: le (plus d h) i
by (subst0_gen_lift_ge . . . . . . H9 H11)
we proved ex2 T λt2:T.eq T t (lift h d t2) λt2:T.subst0 (minus i h) u x0 t2
we proceed by induction on the previous result to prove ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
case ex_intro2 : x1:T H12:eq T t (lift h d x1) H13:subst0 (minus i h) u x0 x1 ⇒
the thesis becomes ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
by (getl_drop_conf_ge . . . H1 . . . H5 H11)
we proved getl (minus i h) e (CHead d0 (Bind Abbr) u)
by (pr2_delta . . . . previous . . H8 . H13)
we proved pr2 e t1 x1
by (ex_intro2 . . . . H12 previous)
ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
we proved ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
(le (plus d h) i)→(ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3)
end of h2
by (lt_le_e . . . h1 h2)
we proved ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
(le d i)→(ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3)
end of h2
by (lt_le_e . . . h1 h2)
ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
we proved ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3
∀H4:(eq T t0 (lift h d t1)).∀e:C.∀H5:(drop h d c0 e).(ex2 T λt3:T.eq T t (lift h d t3) λt3:T.pr2 e t1 t3)
we proved
eq T y (lift h d t1)
→∀e:C.(drop h d c e)→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr2 e t1 t2)
we proved
∀y:T
.pr2 c y x
→(eq T y (lift h d t1)
→∀e:C.(drop h d c e)→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr2 e t1 t2))
by (insert_eq . . . . previous H)
we proved ∀e:C.(drop h d c e)→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr2 e t1 t2)
we proved
∀c:C
.∀t1:T
.∀x:T
.∀h:nat
.∀d:nat
.pr2 c (lift h d t1) x
→∀e:C.(drop h d c e)→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr2 e t1 t2)