DEFINITION sn3_gen_lift()
TYPE =
∀c1:C.∀t:T.∀h:nat.∀d:nat.(sn3 c1 (lift h d t))→∀c2:C.(drop h d c1 c2)→(sn3 c2 t)
BODY =
assume c1: C
assume t: T
assume h: nat
assume d: nat
suppose H: sn3 c1 (lift h d t)
assume y: T
suppose H0: sn3 c1 y
we proceed by induction on H0 to prove ∀x:T.(eq T y (lift h d x))→∀c2:C.(drop h d c1 c2)→(sn3 c2 x)
case sn3_sing : t1:T H1:∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c1 t1 t2)→(sn3 c1 t2) ⇒
the thesis becomes ∀x:T.∀H3:(eq T t1 (lift h d x)).∀c2:C.∀H4:(drop h d c1 c2).(sn3 c2 x)
(H2) by induction hypothesis we know
∀t2:T
.(eq T t1 t2)→∀P:Prop.P
→(pr3 c1 t1 t2)→∀x:T.(eq T t2 (lift h d x))→∀c2:C.(drop h d c1 c2)→(sn3 c2 x)
assume x: T
suppose H3: eq T t1 (lift h d x)
assume c2: C
suppose H4: drop h d c1 c2
(H5)
we proceed by induction on H3 to prove
∀t2:T
.(eq T (lift h d x) t2)→∀P:Prop.P
→(pr3 c1 (lift h d x) t2
→∀x0:T.(eq T t2 (lift h d x0))→∀c3:C.(drop h d c1 c3)→(sn3 c3 x0))
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀t2:T
.(eq T (lift h d x) t2)→∀P:Prop.P
→(pr3 c1 (lift h d x) t2
→∀x0:T.(eq T t2 (lift h d x0))→∀c3:C.(drop h d c1 c3)→(sn3 c3 x0))
end of H5
assume t2: T
suppose H7: (eq T x t2)→∀P:Prop.P
suppose H8: pr3 c2 x t2
(h1)
suppose H9: eq T (lift h d x) (lift h d t2)
assume P: Prop
(H11)
by (lift_inj . . . . H9)
we proved eq T x t2
by (eq_ind_r . . . H7 . previous)
(eq T x x)→∀P0:Prop.P0
end of H11
by (refl_equal . .)
we proved eq T x x
by (H11 previous .)
we proved P
(eq T (lift h d x) (lift h d t2))→∀P:Prop.P
end of h1
(h2)
by (pr3_lift . . . . H4 . . H8)
pr3 c1 (lift h d x) (lift h d t2)
end of h2
(h3)
by (refl_equal . .)
eq T (lift h d t2) (lift h d t2)
end of h3
by (H5 . h1 h2 . h3 . H4)
we proved sn3 c2 t2
we proved ∀t2:T.((eq T x t2)→∀P:Prop.P)→(pr3 c2 x t2)→(sn3 c2 t2)
by (sn3_sing . . previous)
we proved sn3 c2 x
∀x:T.∀H3:(eq T t1 (lift h d x)).∀c2:C.∀H4:(drop h d c1 c2).(sn3 c2 x)
we proved ∀x:T.(eq T y (lift h d x))→∀c2:C.(drop h d c1 c2)→(sn3 c2 x)
by (unintro . . . previous)
we proved (eq T y (lift h d t))→∀c2:C.(drop h d c1 c2)→(sn3 c2 t)
we proved ∀y:T.(sn3 c1 y)→(eq T y (lift h d t))→∀c2:C.(drop h d c1 c2)→(sn3 c2 t)
by (insert_eq . . . . previous H)
we proved ∀c2:C.(drop h d c1 c2)→(sn3 c2 t)
we proved ∀c1:C.∀t:T.∀h:nat.∀d:nat.(sn3 c1 (lift h d t))→∀c2:C.(drop h d c1 c2)→(sn3 c2 t)