DEFINITION ty3_gen_lift()
TYPE =
∀g:G
.∀c:C
.∀t1:T
.∀x:T
.∀h:nat
.∀d:nat
.ty3 g c (lift h d t1) x
→∀e:C.(drop h d c e)→(ex2 T λt2:T.pc3 c (lift h d t2) x λt2:T.ty3 g e t1 t2)
BODY =
assume g: G
assume c: C
assume t1: T
assume x: T
assume h: nat
assume d: nat
suppose H: ty3 g c (lift h d t1) x
assume y: T
suppose H0: ty3 g c y x
we proceed by induction on H0 to prove
∀x0:T
.∀x1:nat
.eq T y (lift h x1 x0)
→∀e:C.(drop h x1 c e)→(ex2 T λt2:T.pc3 c (lift h x1 t2) x λt2:T.ty3 g e x0 t2)
case ty3_conv : c0:C t2:T t:T :ty3 g c0 t2 t u:T t3:T H3:ty3 g c0 u t3 H5:pc3 c0 t3 t2 ⇒
the thesis becomes ∀x0:T.∀x1:nat.∀H6:(eq T u (lift h x1 x0)).∀e:C.∀H7:(drop h x1 c0 e).(ex2 T λt4:T.pc3 c0 (lift h x1 t4) t2 λt4:T.ty3 g e x0 t4)
() by induction hypothesis we know
∀x0:T
.∀x1:nat
.eq T t2 (lift h x1 x0)
→∀e:C.(drop h x1 c0 e)→(ex2 T λt3:T.pc3 c0 (lift h x1 t3) t λt3:T.ty3 g e x0 t3)
(H4) by induction hypothesis we know
∀x0:T
.∀x1:nat
.eq T u (lift h x1 x0)
→∀e:C.(drop h x1 c0 e)→(ex2 T λt4:T.pc3 c0 (lift h x1 t4) t3 λt4:T.ty3 g e x0 t4)
assume x0: T
assume x1: nat
suppose H6: eq T u (lift h x1 x0)
assume e: C
suppose H7: drop h x1 c0 e
(H8)
we proceed by induction on H6 to prove
∀x2:T
.∀x3:nat
.eq T (lift h x1 x0) (lift h x3 x2)
→∀e0:C.(drop h x3 c0 e0)→(ex2 T λt4:T.pc3 c0 (lift h x3 t4) t3 λt4:T.ty3 g e0 x2 t4)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
∀x2:T
.∀x3:nat
.eq T (lift h x1 x0) (lift h x3 x2)
→∀e0:C.(drop h x3 c0 e0)→(ex2 T λt4:T.pc3 c0 (lift h x3 t4) t3 λt4:T.ty3 g e0 x2 t4)
end of H8
(H10)
by (refl_equal . .)
we proved eq T (lift h x1 x0) (lift h x1 x0)
by (H8 . . previous . H7)
ex2 T λt4:T.pc3 c0 (lift h x1 t4) t3 λt4:T.ty3 g e x0 t4
end of H10
we proceed by induction on H10 to prove ex2 T λt4:T.pc3 c0 (lift h x1 t4) t2 λt4:T.ty3 g e x0 t4
case ex_intro2 : x2:T H11:pc3 c0 (lift h x1 x2) t3 H12:ty3 g e x0 x2 ⇒
the thesis becomes ex2 T λt4:T.pc3 c0 (lift h x1 t4) t2 λt4:T.ty3 g e x0 t4
by (pc3_t . . . H11 . H5)
we proved pc3 c0 (lift h x1 x2) t2
by (ex_intro2 . . . . previous H12)
ex2 T λt4:T.pc3 c0 (lift h x1 t4) t2 λt4:T.ty3 g e x0 t4
we proved ex2 T λt4:T.pc3 c0 (lift h x1 t4) t2 λt4:T.ty3 g e x0 t4
∀x0:T.∀x1:nat.∀H6:(eq T u (lift h x1 x0)).∀e:C.∀H7:(drop h x1 c0 e).(ex2 T λt4:T.pc3 c0 (lift h x1 t4) t2 λt4:T.ty3 g e x0 t4)
case ty3_sort : c0:C m:nat ⇒
the thesis becomes
∀x0:T
.∀x1:nat
.∀H1:eq T (TSort m) (lift h x1 x0)
.∀e:C.(drop h x1 c0 e)→(ex2 T λt2:T.pc3 c0 (lift h x1 t2) (TSort (next g m)) λt2:T.ty3 g e x0 t2)
assume x0: T
assume x1: nat
suppose H1: eq T (TSort m) (lift h x1 x0)
assume e: C
suppose : drop h x1 c0 e
(h1)
(h1)
(h1)
by (pc3_refl . .)
pc3 c0 (TSort (next g m)) (TSort (next g m))
end of h1
(h2)
by (lift_sort . . .)
eq T (lift h x1 (TSort (next g m))) (TSort (next g m))
end of h2
by (eq_ind_r . . . h1 . h2)
pc3 c0 (lift h x1 (TSort (next g m))) (TSort (next g m))
end of h1
(h2)
by (ty3_sort . . .)
ty3 g e (TSort m) (TSort (next g m))
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (TSort (next g m)) λt2:T.ty3 g e (TSort m) t2
end of h1
(h2)
by (lift_gen_sort . . . . H1)
eq T x0 (TSort m)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 T λt2:T.pc3 c0 (lift h x1 t2) (TSort (next g m)) λt2:T.ty3 g e x0 t2
∀x0:T
.∀x1:nat
.∀H1:eq T (TSort m) (lift h x1 x0)
.∀e:C.(drop h x1 c0 e)→(ex2 T λt2:T.pc3 c0 (lift h x1 t2) (TSort (next g m)) λt2:T.ty3 g e x0 t2)
case ty3_abbr : n:nat c0:C d0:C u:T H1:getl n c0 (CHead d0 (Bind Abbr) u) t:T H2:ty3 g d0 u t ⇒
the thesis becomes
∀x0:T
.∀x1:nat
.∀H4:eq T (TLRef n) (lift h x1 x0)
.∀e:C.∀H5:(drop h x1 c0 e).(ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2)
(H3) by induction hypothesis we know
∀x0:T
.∀x1:nat
.eq T u (lift h x1 x0)
→∀e:C.(drop h x1 d0 e)→(ex2 T λt2:T.pc3 d0 (lift h x1 t2) t λt2:T.ty3 g e x0 t2)
assume x0: T
assume x1: nat
suppose H4: eq T (TLRef n) (lift h x1 x0)
assume e: C
suppose H5: drop h x1 c0 e
(H_x)
by (lift_gen_lref . . . . H4)
or
land (lt n x1) (eq T x0 (TLRef n))
land (le (plus x1 h) n) (eq T x0 (TLRef (minus n h)))
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2
case or_introl : H7:land (lt n x1) (eq T x0 (TLRef n)) ⇒
the thesis becomes ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2
we proceed by induction on H7 to prove ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2
case conj : H8:lt n x1 H9:eq T x0 (TLRef n) ⇒
the thesis becomes ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2
(H10)
by (lt_plus_minus . . H8)
we proved eq nat x1 (S (plus n (minus x1 (S n))))
we proceed by induction on the previous result to prove drop h (S (plus n (minus x1 (S n)))) c0 e
case refl_equal : ⇒
the thesis becomes the hypothesis H5
drop h (S (plus n (minus x1 (S n)))) c0 e
end of H10
by (getl_drop_conf_lt . . . . . H1 . . . H10)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (minus x1 (S n)) v)
λv:T.λe0:C.getl n e (CHead e0 (Bind Abbr) v)
λ:T.λe0:C.drop h (minus x1 (S n)) d0 e0
we proceed by induction on the previous result to prove ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e (TLRef n) t2
case ex3_2_intro : x2:T x3:C H11:eq T u (lift h (minus x1 (S n)) x2) H12:getl n e (CHead x3 (Bind Abbr) x2) H13:drop h (minus x1 (S n)) d0 x3 ⇒
the thesis becomes ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e (TLRef n) t2
(H14)
we proceed by induction on H11 to prove
∀x4:T
.∀x5:nat
.eq T (lift h (minus x1 (S n)) x2) (lift h x5 x4)
→∀e0:C.(drop h x5 d0 e0)→(ex2 T λt2:T.pc3 d0 (lift h x5 t2) t λt2:T.ty3 g e0 x4 t2)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀x4:T
.∀x5:nat
.eq T (lift h (minus x1 (S n)) x2) (lift h x5 x4)
→∀e0:C.(drop h x5 d0 e0)→(ex2 T λt2:T.pc3 d0 (lift h x5 t2) t λt2:T.ty3 g e0 x4 t2)
end of H14
(H16)
by (refl_equal . .)
we proved eq T (lift h (minus x1 (S n)) x2) (lift h (minus x1 (S n)) x2)
by (H14 . . previous . H13)
ex2 T λt2:T.pc3 d0 (lift h (minus x1 (S n)) t2) t λt2:T.ty3 g x3 x2 t2
end of H16
we proceed by induction on H16 to prove ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e (TLRef n) t2
case ex_intro2 : x4:T H17:pc3 d0 (lift h (minus x1 (S n)) x4) t H18:ty3 g x3 x2 x4 ⇒
the thesis becomes ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e (TLRef n) t2
(h1)
(h1)
(h1)
by (getl_drop . . . . . H1)
we proved drop (S n) O c0 d0
by (pc3_lift . . . . previous . . H17)
pc3 c0 (lift (S n) O (lift h (minus x1 (S n)) x4)) (lift (S n) O t)
end of h1
(h2)
by (le_O_n .)
we proved le O (minus x1 (S n))
by (lift_d . . . . . previous)
eq
T
lift h (plus (S n) (minus x1 (S n))) (lift (S n) O x4)
lift (S n) O (lift h (minus x1 (S n)) x4)
end of h2
by (eq_ind_r . . . h1 . h2)
pc3
c0
lift h (plus (S n) (minus x1 (S n))) (lift (S n) O x4)
lift (S n) O t
end of h1
(h2)
by (ty3_abbr . . . . . H12 . H18)
ty3 g e (TLRef n) (lift (S n) O x4)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt2:T.pc3 c0 (lift h (plus (S n) (minus x1 (S n))) t2) (lift (S n) O t)
λt2:T.ty3 g e (TLRef n) t2
end of h1
(h2)
consider H8
we proved lt n x1
that is equivalent to le (S n) x1
by (le_plus_minus . . previous)
eq nat x1 (plus (S n) (minus x1 (S n)))
end of h2
by (eq_ind_r . . . h1 . h2)
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e (TLRef n) t2
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e (TLRef n) t2
we proved ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e (TLRef n) t2
by (eq_ind_r . . . previous . H9)
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2
case or_intror : H7:land (le (plus x1 h) n) (eq T x0 (TLRef (minus n h))) ⇒
the thesis becomes ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2
we proceed by induction on H7 to prove ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2
case conj : H8:le (plus x1 h) n H9:eq T x0 (TLRef (minus n h)) ⇒
the thesis becomes ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2
(h1)
(h1)
by (plus_n_Sm . .)
we proved eq nat (S (plus h (minus n h))) (plus h (S (minus n h)))
we proceed by induction on the previous result to prove pc3 c0 (lift (plus h (S (minus n h))) O t) (lift (S n) O t)
case refl_equal : ⇒
the thesis becomes pc3 c0 (lift (S (plus h (minus n h))) O t) (lift (S n) O t)
by (le_plus_r . .)
we proved le h (plus x1 h)
by (le_trans . . . previous H8)
we proved le h n
by (le_plus_minus . . previous)
we proved eq nat n (plus h (minus n h))
we proceed by induction on the previous result to prove pc3 c0 (lift (S (plus h (minus n h))) O t) (lift (S n) O t)
case refl_equal : ⇒
the thesis becomes pc3 c0 (lift (S n) O t) (lift (S n) O t)
by (pc3_refl . .)
pc3 c0 (lift (S n) O t) (lift (S n) O t)
pc3 c0 (lift (S (plus h (minus n h))) O t) (lift (S n) O t)
pc3 c0 (lift (plus h (S (minus n h))) O t) (lift (S n) O t)
end of h1
(h2)
(h1)
(h1)
by (le_S_minus . . . H8)
le x1 (S (minus n h))
end of h1
(h2)
by (le_n .)
we proved le (plus O (S (minus n h))) (plus O (S (minus n h)))
le (S (minus n h)) (plus O (S (minus n h)))
end of h2
by (le_trans . . . h1 h2)
le x1 (plus O (S (minus n h)))
end of h1
(h2) by (le_O_n .) we proved le O x1
by (lift_free . . . . . h1 h2)
eq
T
lift h x1 (lift (S (minus n h)) O t)
lift (plus h (S (minus n h))) O t
end of h2
by (eq_ind_r . . . h1 . h2)
pc3 c0 (lift h x1 (lift (S (minus n h)) O t)) (lift (S n) O t)
end of h1
(h2)
by (getl_drop_conf_ge . . . H1 . . . H5 H8)
we proved getl (minus n h) e (CHead d0 (Bind Abbr) u)
by (ty3_abbr . . . . . previous . H2)
ty3 g e (TLRef (minus n h)) (lift (S (minus n h)) O t)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e (TLRef (minus n h)) t2
by (eq_ind_r . . . previous . H9)
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2
we proved ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2
∀x0:T
.∀x1:nat
.∀H4:eq T (TLRef n) (lift h x1 x0)
.∀e:C.∀H5:(drop h x1 c0 e).(ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O t) λt2:T.ty3 g e x0 t2)
case ty3_abst : n:nat c0:C d0:C u:T H1:getl n c0 (CHead d0 (Bind Abst) u) t:T H2:ty3 g d0 u t ⇒
the thesis becomes
∀x0:T
.∀x1:nat
.∀H4:eq T (TLRef n) (lift h x1 x0)
.∀e:C.∀H5:(drop h x1 c0 e).(ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2)
(H3) by induction hypothesis we know
∀x0:T
.∀x1:nat
.eq T u (lift h x1 x0)
→∀e:C.(drop h x1 d0 e)→(ex2 T λt2:T.pc3 d0 (lift h x1 t2) t λt2:T.ty3 g e x0 t2)
assume x0: T
assume x1: nat
suppose H4: eq T (TLRef n) (lift h x1 x0)
assume e: C
suppose H5: drop h x1 c0 e
(H_x)
by (lift_gen_lref . . . . H4)
or
land (lt n x1) (eq T x0 (TLRef n))
land (le (plus x1 h) n) (eq T x0 (TLRef (minus n h)))
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2
case or_introl : H7:land (lt n x1) (eq T x0 (TLRef n)) ⇒
the thesis becomes ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2
we proceed by induction on H7 to prove ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2
case conj : H8:lt n x1 H9:eq T x0 (TLRef n) ⇒
the thesis becomes ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2
(H10)
by (lt_plus_minus . . H8)
we proved eq nat x1 (S (plus n (minus x1 (S n))))
we proceed by induction on the previous result to prove drop h (S (plus n (minus x1 (S n)))) c0 e
case refl_equal : ⇒
the thesis becomes the hypothesis H5
drop h (S (plus n (minus x1 (S n)))) c0 e
end of H10
by (getl_drop_conf_lt . . . . . H1 . . . H10)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift h (minus x1 (S n)) v)
λv:T.λe0:C.getl n e (CHead e0 (Bind Abst) v)
λ:T.λe0:C.drop h (minus x1 (S n)) d0 e0
we proceed by induction on the previous result to prove ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e (TLRef n) t2
case ex3_2_intro : x2:T x3:C H11:eq T u (lift h (minus x1 (S n)) x2) H12:getl n e (CHead x3 (Bind Abst) x2) H13:drop h (minus x1 (S n)) d0 x3 ⇒
the thesis becomes ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e (TLRef n) t2
(H14)
we proceed by induction on H11 to prove
∀x4:T
.∀x5:nat
.eq T (lift h (minus x1 (S n)) x2) (lift h x5 x4)
→∀e0:C.(drop h x5 d0 e0)→(ex2 T λt2:T.pc3 d0 (lift h x5 t2) t λt2:T.ty3 g e0 x4 t2)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀x4:T
.∀x5:nat
.eq T (lift h (minus x1 (S n)) x2) (lift h x5 x4)
→∀e0:C.(drop h x5 d0 e0)→(ex2 T λt2:T.pc3 d0 (lift h x5 t2) t λt2:T.ty3 g e0 x4 t2)
end of H14
(H16)
by (refl_equal . .)
we proved eq T (lift h (minus x1 (S n)) x2) (lift h (minus x1 (S n)) x2)
by (H14 . . previous . H13)
ex2 T λt2:T.pc3 d0 (lift h (minus x1 (S n)) t2) t λt2:T.ty3 g x3 x2 t2
end of H16
we proceed by induction on H16 to prove
ex2
T
λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O (lift h (minus x1 (S n)) x2))
λt2:T.ty3 g e (TLRef n) t2
case ex_intro2 : x4:T :pc3 d0 (lift h (minus x1 (S n)) x4) t H18:ty3 g x3 x2 x4 ⇒
the thesis becomes
ex2
T
λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O (lift h (minus x1 (S n)) x2))
λt2:T.ty3 g e (TLRef n) t2
(h1)
(h1)
(h1)
consider H8
we proved lt n x1
that is equivalent to le (S n) x1
by (le_plus_minus . . previous)
we proved eq nat x1 (plus (S n) (minus x1 (S n)))
we proceed by induction on the previous result to prove
pc3
c0
lift (S n) O (lift h (minus x1 (S n)) x2)
lift
S n
O
lift h (minus (plus (S n) (minus x1 (S n))) (S n)) x2
case refl_equal : ⇒
the thesis becomes
pc3
c0
lift (S n) O (lift h (minus x1 (S n)) x2)
lift (S n) O (lift h (minus x1 (S n)) x2)
by (pc3_refl . .)
pc3
c0
lift (S n) O (lift h (minus x1 (S n)) x2)
lift (S n) O (lift h (minus x1 (S n)) x2)
pc3
c0
lift (S n) O (lift h (minus x1 (S n)) x2)
lift
S n
O
lift h (minus (plus (S n) (minus x1 (S n))) (S n)) x2
end of h1
(h2)
by (le_O_n .)
we proved le O (minus x1 (S n))
by (lift_d . . . . . previous)
eq
T
lift h (plus (S n) (minus x1 (S n))) (lift (S n) O x2)
lift (S n) O (lift h (minus x1 (S n)) x2)
end of h2
by (eq_ind_r . . . h1 . h2)
pc3
c0
lift h (plus (S n) (minus x1 (S n))) (lift (S n) O x2)
lift
S n
O
lift h (minus (plus (S n) (minus x1 (S n))) (S n)) x2
end of h1
(h2)
by (ty3_abst . . . . . H12 . H18)
ty3 g e (TLRef n) (lift (S n) O x2)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt2:T
.pc3
c0
lift h (plus (S n) (minus x1 (S n))) t2
lift
S n
O
lift h (minus (plus (S n) (minus x1 (S n))) (S n)) x2
λt2:T.ty3 g e (TLRef n) t2
end of h1
(h2)
consider H8
we proved lt n x1
that is equivalent to le (S n) x1
by (le_plus_minus . . previous)
eq nat x1 (plus (S n) (minus x1 (S n)))
end of h2
by (eq_ind_r . . . h1 . h2)
ex2
T
λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O (lift h (minus x1 (S n)) x2))
λt2:T.ty3 g e (TLRef n) t2
we proved
ex2
T
λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O (lift h (minus x1 (S n)) x2))
λt2:T.ty3 g e (TLRef n) t2
by (eq_ind_r . . . previous . H11)
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e (TLRef n) t2
we proved ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e (TLRef n) t2
by (eq_ind_r . . . previous . H9)
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2
case or_intror : H7:land (le (plus x1 h) n) (eq T x0 (TLRef (minus n h))) ⇒
the thesis becomes ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2
we proceed by induction on H7 to prove ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2
case conj : H8:le (plus x1 h) n H9:eq T x0 (TLRef (minus n h)) ⇒
the thesis becomes ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2
(h1)
(h1)
by (plus_n_Sm . .)
we proved eq nat (S (plus h (minus n h))) (plus h (S (minus n h)))
we proceed by induction on the previous result to prove pc3 c0 (lift (plus h (S (minus n h))) O u) (lift (S n) O u)
case refl_equal : ⇒
the thesis becomes pc3 c0 (lift (S (plus h (minus n h))) O u) (lift (S n) O u)
by (le_plus_r . .)
we proved le h (plus x1 h)
by (le_trans . . . previous H8)
we proved le h n
by (le_plus_minus . . previous)
we proved eq nat n (plus h (minus n h))
we proceed by induction on the previous result to prove pc3 c0 (lift (S (plus h (minus n h))) O u) (lift (S n) O u)
case refl_equal : ⇒
the thesis becomes pc3 c0 (lift (S n) O u) (lift (S n) O u)
by (pc3_refl . .)
pc3 c0 (lift (S n) O u) (lift (S n) O u)
pc3 c0 (lift (S (plus h (minus n h))) O u) (lift (S n) O u)
pc3 c0 (lift (plus h (S (minus n h))) O u) (lift (S n) O u)
end of h1
(h2)
(h1)
(h1)
by (le_S_minus . . . H8)
le x1 (S (minus n h))
end of h1
(h2)
by (le_n .)
we proved le (plus O (S (minus n h))) (plus O (S (minus n h)))
le (S (minus n h)) (plus O (S (minus n h)))
end of h2
by (le_trans . . . h1 h2)
le x1 (plus O (S (minus n h)))
end of h1
(h2) by (le_O_n .) we proved le O x1
by (lift_free . . . . . h1 h2)
eq
T
lift h x1 (lift (S (minus n h)) O u)
lift (plus h (S (minus n h))) O u
end of h2
by (eq_ind_r . . . h1 . h2)
pc3 c0 (lift h x1 (lift (S (minus n h)) O u)) (lift (S n) O u)
end of h1
(h2)
by (getl_drop_conf_ge . . . H1 . . . H5 H8)
we proved getl (minus n h) e (CHead d0 (Bind Abst) u)
by (ty3_abst . . . . . previous . H2)
ty3 g e (TLRef (minus n h)) (lift (S (minus n h)) O u)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e (TLRef (minus n h)) t2
by (eq_ind_r . . . previous . H9)
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2
we proved ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2
∀x0:T
.∀x1:nat
.∀H4:eq T (TLRef n) (lift h x1 x0)
.∀e:C.∀H5:(drop h x1 c0 e).(ex2 T λt2:T.pc3 c0 (lift h x1 t2) (lift (S n) O u) λt2:T.ty3 g e x0 t2)
case ty3_bind : c0:C u:T t:T H1:ty3 g c0 u t b:B t2:T t3:T H3:ty3 g (CHead c0 (Bind b) u) t2 t3 ⇒
the thesis becomes
∀x0:T
.∀x1:nat
.∀H5:eq T (THead (Bind b) u t2) (lift h x1 x0)
.∀e:C.∀H6:(drop h x1 c0 e).(ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) u t3) λt4:T.ty3 g e x0 t4)
(H2) by induction hypothesis we know
∀x0:T
.∀x1:nat
.eq T u (lift h x1 x0)
→∀e:C.(drop h x1 c0 e)→(ex2 T λt2:T.pc3 c0 (lift h x1 t2) t λt2:T.ty3 g e x0 t2)
(H4) by induction hypothesis we know
∀x0:T
.∀x1:nat
.eq T t2 (lift h x1 x0)
→∀e:C
.drop h x1 (CHead c0 (Bind b) u) e
→ex2 T λt4:T.pc3 (CHead c0 (Bind b) u) (lift h x1 t4) t3 λt4:T.ty3 g e x0 t4
assume x0: T
assume x1: nat
suppose H5: eq T (THead (Bind b) u t2) (lift h x1 x0)
assume e: C
suppose H6: drop h x1 c0 e
by (lift_gen_bind . . . . . . H5)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x0 (THead (Bind b) y z)
λy:T.λ:T.eq T u (lift h x1 y)
λ:T.λz:T.eq T t2 (lift h (S x1) z)
we proceed by induction on the previous result to prove ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) u t3) λt4:T.ty3 g e x0 t4
case ex3_2_intro : x2:T x3:T H7:eq T x0 (THead (Bind b) x2 x3) H8:eq T u (lift h x1 x2) H9:eq T t2 (lift h (S x1) x3) ⇒
the thesis becomes ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) u t3) λt4:T.ty3 g e x0 t4
(H10)
we proceed by induction on H9 to prove
∀x4:T
.∀x5:nat
.eq T (lift h (S x1) x3) (lift h x5 x4)
→∀e0:C
.drop h x5 (CHead c0 (Bind b) u) e0
→ex2 T λt4:T.pc3 (CHead c0 (Bind b) u) (lift h x5 t4) t3 λt4:T.ty3 g e0 x4 t4
case refl_equal : ⇒
the thesis becomes the hypothesis H4
∀x4:T
.∀x5:nat
.eq T (lift h (S x1) x3) (lift h x5 x4)
→∀e0:C
.drop h x5 (CHead c0 (Bind b) u) e0
→ex2 T λt4:T.pc3 (CHead c0 (Bind b) u) (lift h x5 t4) t3 λt4:T.ty3 g e0 x4 t4
end of H10
(H11)
we proceed by induction on H9 to prove ty3 g (CHead c0 (Bind b) u) (lift h (S x1) x3) t3
case refl_equal : ⇒
the thesis becomes the hypothesis H3
ty3 g (CHead c0 (Bind b) u) (lift h (S x1) x3) t3
end of H11
(H13)
we proceed by induction on H8 to prove
∀x4:T
.∀x5:nat
.eq T (lift h (S x1) x3) (lift h x5 x4)
→∀e0:C
.drop h x5 (CHead c0 (Bind b) (lift h x1 x2)) e0
→ex2 T λt4:T.pc3 (CHead c0 (Bind b) (lift h x1 x2)) (lift h x5 t4) t3 λt4:T.ty3 g e0 x4 t4
case refl_equal : ⇒
the thesis becomes the hypothesis H10
∀x4:T
.∀x5:nat
.eq T (lift h (S x1) x3) (lift h x5 x4)
→∀e0:C
.drop h x5 (CHead c0 (Bind b) (lift h x1 x2)) e0
→ex2 T λt4:T.pc3 (CHead c0 (Bind b) (lift h x1 x2)) (lift h x5 t4) t3 λt4:T.ty3 g e0 x4 t4
end of H13
(H14)
we proceed by induction on H8 to prove
∀x4:T
.∀x5:nat
.eq T (lift h x1 x2) (lift h x5 x4)
→∀e0:C.(drop h x5 c0 e0)→(ex2 T λt4:T.pc3 c0 (lift h x5 t4) t λt4:T.ty3 g e0 x4 t4)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀x4:T
.∀x5:nat
.eq T (lift h x1 x2) (lift h x5 x4)
→∀e0:C.(drop h x5 c0 e0)→(ex2 T λt4:T.pc3 c0 (lift h x5 t4) t λt4:T.ty3 g e0 x4 t4)
end of H14
(H16)
by (refl_equal . .)
we proved eq T (lift h x1 x2) (lift h x1 x2)
by (H14 . . previous . H6)
ex2 T λt4:T.pc3 c0 (lift h x1 t4) t λt4:T.ty3 g e x2 t4
end of H16
we proceed by induction on H16 to prove
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3)
λt4:T.ty3 g e (THead (Bind b) x2 x3) t4
case ex_intro2 : x4:T :pc3 c0 (lift h x1 x4) t H18:ty3 g e x2 x4 ⇒
the thesis becomes
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3)
λt4:T.ty3 g e (THead (Bind b) x2 x3) t4
(H19)
(h1)
by (refl_equal . .)
eq T (lift h (S x1) x3) (lift h (S x1) x3)
end of h1
(h2)
by (drop_skip_bind . . . . H6 . .)
drop h (S x1) (CHead c0 (Bind b) (lift h x1 x2)) (CHead e (Bind b) x2)
end of h2
by (H13 . . h1 . h2)
ex2
T
λt4:T.pc3 (CHead c0 (Bind b) (lift h x1 x2)) (lift h (S x1) t4) t3
λt4:T.ty3 g (CHead e (Bind b) x2) x3 t4
end of H19
we proceed by induction on H19 to prove
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3)
λt4:T.ty3 g e (THead (Bind b) x2 x3) t4
case ex_intro2 : x5:T H20:pc3 (CHead c0 (Bind b) (lift h x1 x2)) (lift h (S x1) x5) t3 H21:ty3 g (CHead e (Bind b) x2) x3 x5 ⇒
the thesis becomes
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3)
λt4:T.ty3 g e (THead (Bind b) x2 x3) t4
by (ty3_correct . . . . H21)
we proved ex T λt:T.ty3 g (CHead e (Bind b) x2) x5 t
we proceed by induction on the previous result to prove
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3)
λt4:T.ty3 g e (THead (Bind b) x2 x3) t4
case ex_intro : x6:T :ty3 g (CHead e (Bind b) x2) x5 x6 ⇒
the thesis becomes
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3)
λt4:T.ty3 g e (THead (Bind b) x2 x3) t4
(h1)
(h1)
by (pc3_head_2 . . . . . H20)
pc3
c0
THead (Bind b) (lift h x1 x2) (lift h (S x1) x5)
THead (Bind b) (lift h x1 x2) t3
end of h1
(h2)
by (lift_bind . . . . .)
eq
T
lift h x1 (THead (Bind b) x2 x5)
THead (Bind b) (lift h x1 x2) (lift h (S x1) x5)
end of h2
by (eq_ind_r . . . h1 . h2)
pc3 c0 (lift h x1 (THead (Bind b) x2 x5)) (THead (Bind b) (lift h x1 x2) t3)
end of h1
(h2)
by (ty3_bind . . . . H18 . . . H21)
ty3 g e (THead (Bind b) x2 x3) (THead (Bind b) x2 x5)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3)
λt4:T.ty3 g e (THead (Bind b) x2 x3) t4
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3)
λt4:T.ty3 g e (THead (Bind b) x2 x3) t4
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3)
λt4:T.ty3 g e (THead (Bind b) x2 x3) t4
we proved
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3)
λt4:T.ty3 g e (THead (Bind b) x2 x3) t4
by (eq_ind_r . . . previous . H8)
we proved
ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) u t3) λt4:T.ty3 g e (THead (Bind b) x2 x3) t4
by (eq_ind_r . . . previous . H7)
ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) u t3) λt4:T.ty3 g e x0 t4
we proved ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) u t3) λt4:T.ty3 g e x0 t4
∀x0:T
.∀x1:nat
.∀H5:eq T (THead (Bind b) u t2) (lift h x1 x0)
.∀e:C.∀H6:(drop h x1 c0 e).(ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Bind b) u t3) λt4:T.ty3 g e x0 t4)
case ty3_appl : c0:C w:T u:T H1:ty3 g c0 w u v:T t:T H3:ty3 g c0 v (THead (Bind Abst) u t) ⇒
the thesis becomes
∀x0:T
.∀x1:nat
.∀H5:eq T (THead (Flat Appl) w v) (lift h x1 x0)
.∀e:C
.∀H6:drop h x1 c0 e
.ex2
T
λt2:T.pc3 c0 (lift h x1 t2) (THead (Flat Appl) w (THead (Bind Abst) u t))
λt2:T.ty3 g e x0 t2
(H2) by induction hypothesis we know
∀x0:T
.∀x1:nat
.eq T w (lift h x1 x0)
→∀e:C.(drop h x1 c0 e)→(ex2 T λt2:T.pc3 c0 (lift h x1 t2) u λt2:T.ty3 g e x0 t2)
(H4) by induction hypothesis we know
∀x0:T
.∀x1:nat
.eq T v (lift h x1 x0)
→∀e:C
.drop h x1 c0 e
→ex2 T λt2:T.pc3 c0 (lift h x1 t2) (THead (Bind Abst) u t) λt2:T.ty3 g e x0 t2
assume x0: T
assume x1: nat
suppose H5: eq T (THead (Flat Appl) w v) (lift h x1 x0)
assume e: C
suppose H6: drop h x1 c0 e
by (lift_gen_flat . . . . . . H5)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x0 (THead (Flat Appl) y z)
λy:T.λ:T.eq T w (lift h x1 y)
λ:T.λz:T.eq T v (lift h x1 z)
we proceed by induction on the previous result to prove
ex2
T
λt2:T.pc3 c0 (lift h x1 t2) (THead (Flat Appl) w (THead (Bind Abst) u t))
λt2:T.ty3 g e x0 t2
case ex3_2_intro : x2:T x3:T H7:eq T x0 (THead (Flat Appl) x2 x3) H8:eq T w (lift h x1 x2) H9:eq T v (lift h x1 x3) ⇒
the thesis becomes
ex2
T
λt2:T.pc3 c0 (lift h x1 t2) (THead (Flat Appl) w (THead (Bind Abst) u t))
λt2:T.ty3 g e x0 t2
(H10)
we proceed by induction on H9 to prove
∀x4:T
.∀x5:nat
.eq T (lift h x1 x3) (lift h x5 x4)
→∀e0:C
.(drop h x5 c0 e0)→(ex2 T λt2:T.pc3 c0 (lift h x5 t2) (THead (Bind Abst) u t) λt2:T.ty3 g e0 x4 t2)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
∀x4:T
.∀x5:nat
.eq T (lift h x1 x3) (lift h x5 x4)
→∀e0:C
.(drop h x5 c0 e0)→(ex2 T λt2:T.pc3 c0 (lift h x5 t2) (THead (Bind Abst) u t) λt2:T.ty3 g e0 x4 t2)
end of H10
(H12)
we proceed by induction on H8 to prove
∀x4:T
.∀x5:nat
.eq T (lift h x1 x2) (lift h x5 x4)
→∀e0:C.(drop h x5 c0 e0)→(ex2 T λt2:T.pc3 c0 (lift h x5 t2) u λt2:T.ty3 g e0 x4 t2)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀x4:T
.∀x5:nat
.eq T (lift h x1 x2) (lift h x5 x4)
→∀e0:C.(drop h x5 c0 e0)→(ex2 T λt2:T.pc3 c0 (lift h x5 t2) u λt2:T.ty3 g e0 x4 t2)
end of H12
(H14)
by (refl_equal . .)
we proved eq T (lift h x1 x2) (lift h x1 x2)
by (H12 . . previous . H6)
ex2 T λt2:T.pc3 c0 (lift h x1 t2) u λt2:T.ty3 g e x2 t2
end of H14
we proceed by induction on H14 to prove
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
case ex_intro2 : x4:T H15:pc3 c0 (lift h x1 x4) u H16:ty3 g e x2 x4 ⇒
the thesis becomes
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
(H17)
by (refl_equal . .)
we proved eq T (lift h x1 x3) (lift h x1 x3)
by (H10 . . previous . H6)
ex2 T λt2:T.pc3 c0 (lift h x1 t2) (THead (Bind Abst) u t) λt2:T.ty3 g e x3 t2
end of H17
we proceed by induction on H17 to prove
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
case ex_intro2 : x5:T H18:pc3 c0 (lift h x1 x5) (THead (Bind Abst) u t) H19:ty3 g e x3 x5 ⇒
the thesis becomes
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
by (pc3_gen_lift_abst . . . . . . H18 . H6)
we proved
ex3_2
T
T
λu1:T.λt1:T.pr3 e x5 (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c0 u (lift h x1 u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c0 (Bind b) u) t (lift h (S x1) t1))
we proceed by induction on the previous result to prove
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
case ex3_2_intro : x6:T x7:T H20:pr3 e x5 (THead (Bind Abst) x6 x7) H21:pr3 c0 u (lift h x1 x6) H22:∀b:B.∀u0:T.(pr3 (CHead c0 (Bind b) u0) t (lift h (S x1) x7)) ⇒
the thesis becomes
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
by (ty3_correct . . . . H19)
we proved ex T λt:T.ty3 g e x5 t
we proceed by induction on the previous result to prove
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
case ex_intro : x8:T H23:ty3 g e x5 x8 ⇒
the thesis becomes
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
(H_y)
by (ty3_sred_pr3 . . . H20 . . H23)
ty3 g e (THead (Bind Abst) x6 x7) x8
end of H_y
by (ty3_gen_bind . . . . . . H_y)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 e (THead (Bind Abst) x6 t2) x8
λ:T.λt:T.ty3 g e x6 t
λt2:T.λ:T.ty3 g (CHead e (Bind Abst) x6) x7 t2
we proceed by induction on the previous result to prove
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
case ex3_2_intro : x9:T x10:T :pc3 e (THead (Bind Abst) x6 x9) x8 H25:ty3 g e x6 x10 H26:ty3 g (CHead e (Bind Abst) x6) x7 x9 ⇒
the thesis becomes
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
(h1)
(h1)
(h1)
(h1)
by (pc3_pr3_x . . . H21)
pc3 c0 (lift h x1 x6) u
end of h1
(h2)
by (H22 . .)
we proved pr3 (CHead c0 (Bind Abst) (lift h x1 x6)) t (lift h (S x1) x7)
by (pc3_pr3_x . . . previous)
pc3 (CHead c0 (Bind Abst) (lift h x1 x6)) (lift h (S x1) x7) t
end of h2
by (pc3_head_21 . . . h1 . . . h2)
pc3
c0
THead (Bind Abst) (lift h x1 x6) (lift h (S x1) x7)
THead (Bind Abst) u t
end of h1
(h2)
by (lift_bind . . . . .)
eq
T
lift h x1 (THead (Bind Abst) x6 x7)
THead (Bind Abst) (lift h x1 x6) (lift h (S x1) x7)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved pc3 c0 (lift h x1 (THead (Bind Abst) x6 x7)) (THead (Bind Abst) u t)
by (pc3_thin_dx . . . previous . .)
pc3
c0
THead (Flat Appl) (lift h x1 x2) (lift h x1 (THead (Bind Abst) x6 x7))
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
end of h1
(h2)
by (lift_flat . . . . .)
eq
T
lift h x1 (THead (Flat Appl) x2 (THead (Bind Abst) x6 x7))
THead (Flat Appl) (lift h x1 x2) (lift h x1 (THead (Bind Abst) x6 x7))
end of h2
by (eq_ind_r . . . h1 . h2)
pc3
c0
lift h x1 (THead (Flat Appl) x2 (THead (Bind Abst) x6 x7))
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
end of h1
(h2)
(h1)
by (pc3_pr3_r . . . H21)
we proved pc3 c0 u (lift h x1 x6)
by (pc3_t . . . H15 . previous)
we proved pc3 c0 (lift h x1 x4) (lift h x1 x6)
by (pc3_gen_lift . . . . . previous . H6)
we proved pc3 e x4 x6
by (ty3_conv . . . . H25 . . H16 previous)
ty3 g e x2 x6
end of h1
(h2)
(h1)
by (ty3_bind . . . . H25 . . . H26)
ty3 g e (THead (Bind Abst) x6 x7) (THead (Bind Abst) x6 x9)
end of h1
(h2)
by (pc3_pr3_r . . . H20)
pc3 e x5 (THead (Bind Abst) x6 x7)
end of h2
by (ty3_conv . . . . h1 . . H19 h2)
ty3 g e x3 (THead (Bind Abst) x6 x7)
end of h2
by (ty3_appl . . . . h1 . . h2)
ty3
g
e
THead (Flat Appl) x2 x3
THead (Flat Appl) x2 (THead (Bind Abst) x6 x7)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
we proved
ex2
T
λt2:T
.pc3
c0
lift h x1 t2
THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
by (eq_ind_r . . . previous . H8)
we proved
ex2
T
λt2:T.pc3 c0 (lift h x1 t2) (THead (Flat Appl) w (THead (Bind Abst) u t))
λt2:T.ty3 g e (THead (Flat Appl) x2 x3) t2
by (eq_ind_r . . . previous . H7)
ex2
T
λt2:T.pc3 c0 (lift h x1 t2) (THead (Flat Appl) w (THead (Bind Abst) u t))
λt2:T.ty3 g e x0 t2
we proved
ex2
T
λt2:T.pc3 c0 (lift h x1 t2) (THead (Flat Appl) w (THead (Bind Abst) u t))
λt2:T.ty3 g e x0 t2
∀x0:T
.∀x1:nat
.∀H5:eq T (THead (Flat Appl) w v) (lift h x1 x0)
.∀e:C
.∀H6:drop h x1 c0 e
.ex2
T
λt2:T.pc3 c0 (lift h x1 t2) (THead (Flat Appl) w (THead (Bind Abst) u t))
λt2:T.ty3 g e x0 t2
case ty3_cast : c0:C t2:T t3:T H1:ty3 g c0 t2 t3 t0:T H3:ty3 g c0 t3 t0 ⇒
the thesis becomes
∀x0:T
.∀x1:nat
.∀H5:eq T (THead (Flat Cast) t3 t2) (lift h x1 x0)
.∀e:C.∀H6:(drop h x1 c0 e).(ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 t3) λt4:T.ty3 g e x0 t4)
(H2) by induction hypothesis we know
∀x0:T
.∀x1:nat
.eq T t2 (lift h x1 x0)
→∀e:C.(drop h x1 c0 e)→(ex2 T λt4:T.pc3 c0 (lift h x1 t4) t3 λt4:T.ty3 g e x0 t4)
(H4) by induction hypothesis we know
∀x0:T
.∀x1:nat
.eq T t3 (lift h x1 x0)
→∀e:C.(drop h x1 c0 e)→(ex2 T λt4:T.pc3 c0 (lift h x1 t4) t0 λt4:T.ty3 g e x0 t4)
assume x0: T
assume x1: nat
suppose H5: eq T (THead (Flat Cast) t3 t2) (lift h x1 x0)
assume e: C
suppose H6: drop h x1 c0 e
by (lift_gen_flat . . . . . . H5)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x0 (THead (Flat Cast) y z)
λy:T.λ:T.eq T t3 (lift h x1 y)
λ:T.λz:T.eq T t2 (lift h x1 z)
we proceed by induction on the previous result to prove ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 t3) λt4:T.ty3 g e x0 t4
case ex3_2_intro : x2:T x3:T H7:eq T x0 (THead (Flat Cast) x2 x3) H8:eq T t3 (lift h x1 x2) H9:eq T t2 (lift h x1 x3) ⇒
the thesis becomes ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 t3) λt4:T.ty3 g e x0 t4
(H10)
we proceed by induction on H8 to prove
∀x4:T
.∀x5:nat
.eq T (lift h x1 x2) (lift h x5 x4)
→∀e0:C.(drop h x5 c0 e0)→(ex2 T λt4:T.pc3 c0 (lift h x5 t4) t0 λt4:T.ty3 g e0 x4 t4)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
∀x4:T
.∀x5:nat
.eq T (lift h x1 x2) (lift h x5 x4)
→∀e0:C.(drop h x5 c0 e0)→(ex2 T λt4:T.pc3 c0 (lift h x5 t4) t0 λt4:T.ty3 g e0 x4 t4)
end of H10
(H12)
we proceed by induction on H8 to prove
∀x4:T
.∀x5:nat
.eq T t2 (lift h x5 x4)
→∀e0:C.(drop h x5 c0 e0)→(ex2 T λt4:T.pc3 c0 (lift h x5 t4) (lift h x1 x2) λt4:T.ty3 g e0 x4 t4)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀x4:T
.∀x5:nat
.eq T t2 (lift h x5 x4)
→∀e0:C.(drop h x5 c0 e0)→(ex2 T λt4:T.pc3 c0 (lift h x5 t4) (lift h x1 x2) λt4:T.ty3 g e0 x4 t4)
end of H12
(H13)
we proceed by induction on H8 to prove ty3 g c0 t2 (lift h x1 x2)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
ty3 g c0 t2 (lift h x1 x2)
end of H13
(H15)
we proceed by induction on H9 to prove
∀x4:T
.∀x5:nat
.eq T (lift h x1 x3) (lift h x5 x4)
→∀e0:C.(drop h x5 c0 e0)→(ex2 T λt4:T.pc3 c0 (lift h x5 t4) (lift h x1 x2) λt4:T.ty3 g e0 x4 t4)
case refl_equal : ⇒
the thesis becomes the hypothesis H12
∀x4:T
.∀x5:nat
.eq T (lift h x1 x3) (lift h x5 x4)
→∀e0:C.(drop h x5 c0 e0)→(ex2 T λt4:T.pc3 c0 (lift h x5 t4) (lift h x1 x2) λt4:T.ty3 g e0 x4 t4)
end of H15
(H16)
by (refl_equal . .)
we proved eq T (lift h x1 x3) (lift h x1 x3)
by (H15 . . previous . H6)
ex2 T λt4:T.pc3 c0 (lift h x1 t4) (lift h x1 x2) λt4:T.ty3 g e x3 t4
end of H16
we proceed by induction on H16 to prove
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1 x2))
λt4:T.ty3 g e (THead (Flat Cast) x2 x3) t4
case ex_intro2 : x4:T H17:pc3 c0 (lift h x1 x4) (lift h x1 x2) H18:ty3 g e x3 x4 ⇒
the thesis becomes
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1 x2))
λt4:T.ty3 g e (THead (Flat Cast) x2 x3) t4
(H19)
by (refl_equal . .)
we proved eq T (lift h x1 x2) (lift h x1 x2)
by (H10 . . previous . H6)
ex2 T λt4:T.pc3 c0 (lift h x1 t4) t0 λt4:T.ty3 g e x2 t4
end of H19
we proceed by induction on H19 to prove
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1 x2))
λt4:T.ty3 g e (THead (Flat Cast) x2 x3) t4
case ex_intro2 : x5:T H20:pc3 c0 (lift h x1 x5) t0 H21:ty3 g e x2 x5 ⇒
the thesis becomes
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1 x2))
λt4:T.ty3 g e (THead (Flat Cast) x2 x3) t4
(h1)
(h1)
by (pc3_head_1 . . . H20 . .)
pc3
c0
THead (Flat Cast) (lift h x1 x5) (lift h x1 x2)
THead (Flat Cast) t0 (lift h x1 x2)
end of h1
(h2)
by (lift_flat . . . . .)
eq
T
lift h x1 (THead (Flat Cast) x5 x2)
THead (Flat Cast) (lift h x1 x5) (lift h x1 x2)
end of h2
by (eq_ind_r . . . h1 . h2)
pc3
c0
lift h x1 (THead (Flat Cast) x5 x2)
THead (Flat Cast) t0 (lift h x1 x2)
end of h1
(h2)
by (pc3_gen_lift . . . . . H17 . H6)
we proved pc3 e x4 x2
by (ty3_conv . . . . H21 . . H18 previous)
we proved ty3 g e x3 x2
by (ty3_cast . . . . previous . H21)
ty3 g e (THead (Flat Cast) x2 x3) (THead (Flat Cast) x5 x2)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1 x2))
λt4:T.ty3 g e (THead (Flat Cast) x2 x3) t4
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1 x2))
λt4:T.ty3 g e (THead (Flat Cast) x2 x3) t4
we proved
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1 x2))
λt4:T.ty3 g e (THead (Flat Cast) x2 x3) t4
by (eq_ind_r . . . previous . H8)
we proved
ex2
T
λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 t3)
λt4:T.ty3 g e (THead (Flat Cast) x2 x3) t4
by (eq_ind_r . . . previous . H7)
ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 t3) λt4:T.ty3 g e x0 t4
we proved ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 t3) λt4:T.ty3 g e x0 t4
∀x0:T
.∀x1:nat
.∀H5:eq T (THead (Flat Cast) t3 t2) (lift h x1 x0)
.∀e:C.∀H6:(drop h x1 c0 e).(ex2 T λt4:T.pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 t3) λt4:T.ty3 g e x0 t4)
we proved
∀x0:T
.∀x1:nat
.eq T y (lift h x1 x0)
→∀e:C.(drop h x1 c e)→(ex2 T λt2:T.pc3 c (lift h x1 t2) x λt2:T.ty3 g e x0 t2)
by (unintro . . . previous)
we proved
∀x0:nat
.eq T y (lift h x0 t1)
→∀e:C.(drop h x0 c e)→(ex2 T λt2:T.pc3 c (lift h x0 t2) x λt2:T.ty3 g e t1 t2)
by (unintro . . . previous)
we proved
eq T y (lift h d t1)
→∀e:C.(drop h d c e)→(ex2 T λt2:T.pc3 c (lift h d t2) x λt2:T.ty3 g e t1 t2)
we proved
∀y:T
.ty3 g c y x
→(eq T y (lift h d t1)
→∀e:C.(drop h d c e)→(ex2 T λt2:T.pc3 c (lift h d t2) x λt2:T.ty3 g e t1 t2))
by (insert_eq . . . . previous H)
we proved ∀e:C.(drop h d c e)→(ex2 T λt2:T.pc3 c (lift h d t2) x λt2:T.ty3 g e t1 t2)
we proved
∀g:G
.∀c:C
.∀t1:T
.∀x:T
.∀h:nat
.∀d:nat
.ty3 g c (lift h d t1) x
→∀e:C.(drop h d c e)→(ex2 T λt2:T.pc3 c (lift h d t2) x λt2:T.ty3 g e t1 t2)