DEFINITION pr2_lift()
TYPE =
∀c:C
.∀e:C
.∀h:nat
.∀d:nat.(drop h d c e)→∀t1:T.∀t2:T.(pr2 e t1 t2)→(pr2 c (lift h d t1) (lift h d t2))
BODY =
assume c: C
assume e: C
assume h: nat
assume d: nat
suppose H: drop h d c e
assume t1: T
assume t2: T
suppose H0: pr2 e t1 t2
assume y: C
suppose H1: pr2 y t1 t2
we proceed by induction on H1 to prove (eq C y e)→(pr2 c (lift h d t1) (lift h d t2))
case pr2_free : c0:C t3:T t4:T H2:pr0 t3 t4 ⇒
the thesis becomes (eq C c0 e)→(pr2 c (lift h d t3) (lift h d t4))
suppose : eq C c0 e
by (pr0_lift . . H2 . .)
we proved pr0 (lift h d t3) (lift h d t4)
by (pr2_free . . . previous)
we proved pr2 c (lift h d t3) (lift h d t4)
(eq C c0 e)→(pr2 c (lift h d t3) (lift h d t4))
case pr2_delta : c0:C d0:C u:T i:nat H2:getl i c0 (CHead d0 (Bind Abbr) u) t3:T t4:T H3:pr0 t3 t4 t:T H4:subst0 i u t4 t ⇒
the thesis becomes ∀H5:(eq C c0 e).(pr2 c (lift h d t3) (lift h d t))
suppose H5: eq C c0 e
(H6)
we proceed by induction on H5 to prove getl i e (CHead d0 (Bind Abbr) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
getl i e (CHead d0 (Bind Abbr) u)
end of H6
(h1)
suppose H7: lt i d
(H8)
consider H7
we proved lt i d
that is equivalent to le (S i) d
by (le_S . . previous)
we proved le (S i) (S d)
by (le_S_n . . previous)
we proved le i d
by (drop_getl_trans_le . . previous . . . H . H6)
ex3_2
C
C
λe0:C.λ:C.drop i O c e0
λe0:C.λe1:C.drop h (minus d i) e0 e1
λ:C.λe1:C.clear e1 (CHead d0 (Bind Abbr) u)
end of H8
we proceed by induction on H8 to prove pr2 c (lift h d t3) (lift h d t)
case ex3_2_intro : x0:C x1:C H9:drop i O c x0 H10:drop h (minus d i) x0 x1 H11:clear x1 (CHead d0 (Bind Abbr) u) ⇒
the thesis becomes pr2 c (lift h d t3) (lift h d t)
(H12)
by (minus_x_Sy . . H7)
we proved eq nat (minus d i) (S (minus d (S i)))
we proceed by induction on the previous result to prove drop h (S (minus d (S i))) x0 x1
case refl_equal : ⇒
the thesis becomes the hypothesis H10
drop h (S (minus d (S i))) x0 x1
end of H12
(H13)
by (drop_clear_S . . . . H12 . . . H11)
ex2
C
λc1:C.clear x0 (CHead c1 (Bind Abbr) (lift h (minus d (S i)) u))
λc1:C.drop h (minus d (S i)) c1 d0
end of H13
we proceed by induction on H13 to prove pr2 c (lift h d t3) (lift h d t)
case ex_intro2 : x:C H14:clear x0 (CHead x (Bind Abbr) (lift h (minus d (S i)) u)) :drop h (minus d (S i)) x d0 ⇒
the thesis becomes pr2 c (lift h d t3) (lift h d t)
(h1)
by (getl_intro . . . . H9 H14)
getl i c (CHead x (Bind Abbr) (lift h (minus d (S i)) u))
end of h1
(h2)
by (pr0_lift . . H3 . .)
pr0 (lift h d t3) (lift h d t4)
end of h2
(h3)
by (subst0_lift_lt . . . . H4 . H7 .)
subst0 i (lift h (minus d (S i)) u) (lift h d t4) (lift h d t)
end of h3
by (pr2_delta . . . . h1 . . h2 . h3)
pr2 c (lift h d t3) (lift h d t)
pr2 c (lift h d t3) (lift h d t)
we proved pr2 c (lift h d t3) (lift h d t)
(lt i d)→(pr2 c (lift h d t3) (lift h d t))
end of h1
(h2)
suppose H7: le d i
(h1)
by (drop_getl_trans_ge . . . . . H . H6 H7)
getl (plus i h) c (CHead d0 (Bind Abbr) u)
end of h1
(h2)
by (pr0_lift . . H3 . .)
pr0 (lift h d t3) (lift h d t4)
end of h2
(h3)
by (subst0_lift_ge . . . . . H4 . H7)
subst0 (plus i h) u (lift h d t4) (lift h d t)
end of h3
by (pr2_delta . . . . h1 . . h2 . h3)
we proved pr2 c (lift h d t3) (lift h d t)
(le d i)→(pr2 c (lift h d t3) (lift h d t))
end of h2
by (lt_le_e . . . h1 h2)
we proved pr2 c (lift h d t3) (lift h d t)
∀H5:(eq C c0 e).(pr2 c (lift h d t3) (lift h d t))
we proved (eq C y e)→(pr2 c (lift h d t1) (lift h d t2))
we proved ∀y:C.(pr2 y t1 t2)→(eq C y e)→(pr2 c (lift h d t1) (lift h d t2))
by (insert_eq . . . . previous H0)
we proved pr2 c (lift h d t1) (lift h d t2)
we proved
∀c:C
.∀e:C
.∀h:nat
.∀d:nat.(drop h d c e)→∀t1:T.∀t2:T.(pr2 e t1 t2)→(pr2 c (lift h d t1) (lift h d t2))