DEFINITION pr3_gen_lift()
TYPE =
∀c:C
.∀t1:T
.∀x:T
.∀h:nat
.∀d:nat
.pr3 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.pr3 e t1 t2)
BODY =
assume c: C
assume t1: T
assume x: T
assume h: nat
assume d: nat
suppose H: pr3 c (lift h d t1) x
assume y: T
suppose H0: pr3 c y x
we proceed by induction on H0 to prove
∀x0:T
.eq T y (lift h d x0)
→∀e:C.(drop h d c e)→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr3 e x0 t2)
case pr3_refl : t:T ⇒
the thesis becomes
∀x0:T
.∀H1:eq T t (lift h d x0)
.∀e:C.(drop h d c e)→(ex2 T λt2:T.eq T t (lift h d t2) λt2:T.pr3 e x0 t2)
assume x0: T
suppose H1: eq T t (lift h d x0)
assume e: C
suppose : drop h d c e
by (pr3_refl . .)
we proved pr3 e x0 x0
by (ex_intro2 . . . . H1 previous)
we proved ex2 T λt2:T.eq T t (lift h d t2) λt2:T.pr3 e x0 t2
∀x0:T
.∀H1:eq T t (lift h d x0)
.∀e:C.(drop h d c e)→(ex2 T λt2:T.eq T t (lift h d t2) λt2:T.pr3 e x0 t2)
case pr3_sing : t2:T t3:T H1:pr2 c t3 t2 t4:T :pr3 c t2 t4 ⇒
the thesis becomes ∀x0:T.∀H4:(eq T t3 (lift h d x0)).∀e:C.∀H5:(drop h d c e).(ex2 T λt5:T.eq T t4 (lift h d t5) λt5:T.pr3 e x0 t5)
(H3) by induction hypothesis we know
∀x0:T
.eq T t2 (lift h d x0)
→∀e:C.(drop h d c e)→(ex2 T λt5:T.eq T t4 (lift h d t5) λt5:T.pr3 e x0 t5)
assume x0: T
suppose H4: eq T t3 (lift h d x0)
assume e: C
suppose H5: drop h d c e
(H6)
we proceed by induction on H4 to prove pr2 c (lift h d x0) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
pr2 c (lift h d x0) t2
end of H6
(H7)
by (pr2_gen_lift . . . . . H6 . H5)
ex2 T λt2:T.eq T t2 (lift h d t2) λt2:T.pr2 e x0 t2
end of H7
we proceed by induction on H7 to prove ex2 T λt5:T.eq T t4 (lift h d t5) λt5:T.pr3 e x0 t5
case ex_intro2 : x1:T H8:eq T t2 (lift h d x1) H9:pr2 e x0 x1 ⇒
the thesis becomes ex2 T λt5:T.eq T t4 (lift h d t5) λt5:T.pr3 e x0 t5
by (H3 . H8 . H5)
we proved ex2 T λt5:T.eq T t4 (lift h d t5) λt5:T.pr3 e x1 t5
we proceed by induction on the previous result to prove ex2 T λt5:T.eq T t4 (lift h d t5) λt5:T.pr3 e x0 t5
case ex_intro2 : x2:T H10:eq T t4 (lift h d x2) H11:pr3 e x1 x2 ⇒
the thesis becomes ex2 T λt5:T.eq T t4 (lift h d t5) λt5:T.pr3 e x0 t5
by (pr3_sing . . . H9 . H11)
we proved pr3 e x0 x2
by (ex_intro2 . . . . H10 previous)
ex2 T λt5:T.eq T t4 (lift h d t5) λt5:T.pr3 e x0 t5
ex2 T λt5:T.eq T t4 (lift h d t5) λt5:T.pr3 e x0 t5
we proved ex2 T λt5:T.eq T t4 (lift h d t5) λt5:T.pr3 e x0 t5
∀x0:T.∀H4:(eq T t3 (lift h d x0)).∀e:C.∀H5:(drop h d c e).(ex2 T λt5:T.eq T t4 (lift h d t5) λt5:T.pr3 e x0 t5)
we proved
∀x0:T
.eq T y (lift h d x0)
→∀e:C.(drop h d c e)→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr3 e x0 t2)
by (unintro . . . previous)
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.pr3 e t1 t2)
we proved
∀y:T
.pr3 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.pr3 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.pr3 e t1 t2)
we proved
∀c:C
.∀t1:T
.∀x:T
.∀h:nat
.∀d:nat
.pr3 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.pr3 e t1 t2)