DEFINITION ty3_lift()
TYPE =
∀g:G
.∀e:C
.∀t1:T
.∀t2:T
.ty3 g e t1 t2
→∀c:C.∀d:nat.∀h:nat.(drop h d c e)→(ty3 g c (lift h d t1) (lift h d t2))
BODY =
assume g: G
assume e: C
assume t1: T
assume t2: T
suppose H: ty3 g e t1 t2
we proceed by induction on H to prove ∀c0:C.∀d:nat.∀h:nat.(drop h d c0 e)→(ty3 g c0 (lift h d t1) (lift h d t2))
case ty3_conv : c:C t0:T t:T :ty3 g c t0 t u:T t3:T :ty3 g c u t3 H4:pc3 c t3 t0 ⇒
the thesis becomes ∀c0:C.∀d:nat.∀h:nat.∀H5:(drop h d c0 c).(ty3 g c0 (lift h d u) (lift h d t0))
(H1) by induction hypothesis we know ∀c0:C.∀d:nat.∀h:nat.(drop h d c0 c)→(ty3 g c0 (lift h d t0) (lift h d t))
(H3) by induction hypothesis we know ∀c0:C.∀d:nat.∀h:nat.(drop h d c0 c)→(ty3 g c0 (lift h d u) (lift h d t3))
assume c0: C
assume d: nat
assume h: nat
suppose H5: drop h d c0 c
(h1)
by (H1 . . . H5)
ty3 g c0 (lift h d t0) (lift h d t)
end of h1
(h2)
by (H3 . . . H5)
ty3 g c0 (lift h d u) (lift h d t3)
end of h2
(h3)
by (pc3_lift . . . . H5 . . H4)
pc3 c0 (lift h d t3) (lift h d t0)
end of h3
by (ty3_conv . . . . h1 . . h2 h3)
we proved ty3 g c0 (lift h d u) (lift h d t0)
∀c0:C.∀d:nat.∀h:nat.∀H5:(drop h d c0 c).(ty3 g c0 (lift h d u) (lift h d t0))
case ty3_sort : c:C m:nat ⇒
the thesis becomes
∀c0:C
.∀d:nat
.∀h:nat
.drop h d c0 c
→ty3 g c0 (lift h d (TSort m)) (lift h d (TSort (next g m)))
assume c0: C
assume d: nat
assume h: nat
suppose : drop h d c0 c
(h1)
(h1)
by (ty3_sort . . .)
ty3 g c0 (TSort m) (TSort (next g m))
end of h1
(h2)
by (lift_sort . . .)
eq T (lift h d (TSort (next g m))) (TSort (next g m))
end of h2
by (eq_ind_r . . . h1 . h2)
ty3 g c0 (TSort m) (lift h d (TSort (next g m)))
end of h1
(h2)
by (lift_sort . . .)
eq T (lift h d (TSort m)) (TSort m)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ty3 g c0 (lift h d (TSort m)) (lift h d (TSort (next g m)))
∀c0:C
.∀d:nat
.∀h:nat
.drop h d c0 c
→ty3 g c0 (lift h d (TSort m)) (lift h d (TSort (next g m)))
case ty3_abbr : n:nat c:C d:C u:T H0:getl n c (CHead d (Bind Abbr) u) t:T H1:ty3 g d u t ⇒
the thesis becomes
∀c0:C
.∀d0:nat
.∀h:nat
.∀H3:(drop h d0 c0 c).(ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t)))
(H2) by induction hypothesis we know ∀c0:C.∀d0:nat.∀h:nat.(drop h d0 c0 d)→(ty3 g c0 (lift h d0 u) (lift h d0 t))
assume c0: C
assume d0: nat
assume h: nat
suppose H3: drop h d0 c0 c
(h1)
suppose H4: lt n d0
(H5)
consider H4
we proved lt n d0
that is equivalent to le (S n) d0
by (le_S . . previous)
we proved le (S n) (S d0)
by (le_S_n . . previous)
we proved le n d0
by (drop_getl_trans_le . . previous . . . H3 . H0)
ex3_2
C
C
λe0:C.λ:C.drop n O c0 e0
λe0:C.λe1:C.drop h (minus d0 n) e0 e1
λ:C.λe1:C.clear e1 (CHead d (Bind Abbr) u)
end of H5
we proceed by induction on H5 to prove ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t))
case ex3_2_intro : x0:C x1:C H6:drop n O c0 x0 H7:drop h (minus d0 n) x0 x1 H8:clear x1 (CHead d (Bind Abbr) u) ⇒
the thesis becomes ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t))
(H9)
by (minus_x_Sy . . H4)
we proved eq nat (minus d0 n) (S (minus d0 (S n)))
we proceed by induction on the previous result to prove drop h (S (minus d0 (S n))) x0 x1
case refl_equal : ⇒
the thesis becomes the hypothesis H7
drop h (S (minus d0 (S n))) x0 x1
end of H9
(H10)
by (drop_clear_S . . . . H9 . . . H8)
ex2
C
λc1:C.clear x0 (CHead c1 (Bind Abbr) (lift h (minus d0 (S n)) u))
λc1:C.drop h (minus d0 (S n)) c1 d
end of H10
we proceed by induction on H10 to prove ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t))
case ex_intro2 : x:C H11:clear x0 (CHead x (Bind Abbr) (lift h (minus d0 (S n)) u)) H12:drop h (minus d0 (S n)) x d ⇒
the thesis becomes ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t))
(h1)
consider H4
we proved lt n d0
that is equivalent to le (S n) d0
by (le_plus_minus_r . . previous)
we proved eq nat (plus (S n) (minus d0 (S n))) d0
we proceed by induction on the previous result to prove ty3 g c0 (TLRef n) (lift h d0 (lift (S n) O t))
case refl_equal : ⇒
the thesis becomes
ty3
g
c0
TLRef n
lift h (plus (S n) (minus d0 (S n))) (lift (S n) O t)
(h1)
consider H4
we proved lt n d0
that is equivalent to le (S n) d0
by (le_plus_minus . . previous)
we proved eq nat d0 (plus (S n) (minus d0 (S n)))
we proceed by induction on the previous result to prove ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S n)) t))
case refl_equal : ⇒
the thesis becomes ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S n)) t))
(h1)
by (getl_intro . . . . H6 H11)
getl n c0 (CHead x (Bind Abbr) (lift h (minus d0 (S n)) u))
end of h1
(h2)
by (H2 . . . H12)
ty3 g x (lift h (minus d0 (S n)) u) (lift h (minus d0 (S n)) t)
end of h2
by (ty3_abbr . . . . . h1 . h2)
ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S n)) t))
ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S n)) t))
end of h1
(h2)
by (le_O_n .)
we proved le O (minus d0 (S n))
by (lift_d . . . . . previous)
eq
T
lift h (plus (S n) (minus d0 (S n))) (lift (S n) O t)
lift (S n) O (lift h (minus d0 (S n)) t)
end of h2
by (eq_ind_r . . . h1 . h2)
ty3
g
c0
TLRef n
lift h (plus (S n) (minus d0 (S n))) (lift (S n) O t)
ty3 g c0 (TLRef n) (lift h d0 (lift (S n) O t))
end of h1
(h2)
by (lift_lref_lt . . . H4)
eq T (lift h d0 (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t))
ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t))
we proved ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t))
(lt n d0)→(ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t)))
end of h1
(h2)
suppose H4: le d0 n
(h1)
(h1)
by (refl_equal . .)
we proved eq nat (plus (S O) n) (plus (S O) n)
eq nat (S n) (plus (S O) n)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus n (S O)) (plus (S O) n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq nat (S n) (plus n (S O))
we proceed by induction on the previous result to prove ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O t))
case refl_equal : ⇒
the thesis becomes ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O t))
(h1)
(h1)
by (drop_getl_trans_ge . . . . . H3 . H0 H4)
we proved getl (plus n h) c0 (CHead d (Bind Abbr) u)
by (ty3_abbr . . . . . previous . H1)
we proved ty3 g c0 (TLRef (plus n h)) (lift (S (plus n h)) O t)
ty3 g c0 (TLRef (plus n h)) (lift (plus (S n) h) O t)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus h (S n)) (plus (S n) h)
end of h2
by (eq_ind_r . . . h1 . h2)
ty3 g c0 (TLRef (plus n h)) (lift (plus h (S n)) O t)
end of h1
(h2)
(h1)
by (le_S . . H4)
we proved le d0 (S n)
le d0 (plus O (S n))
end of h1
(h2) by (le_O_n .) we proved le O d0
by (lift_free . . . . . h1 h2)
eq T (lift h d0 (lift (S n) O t)) (lift (plus h (S n)) O t)
end of h2
by (eq_ind_r . . . h1 . h2)
ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O t))
ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O t))
end of h1
(h2)
by (lift_lref_ge . . . H4)
eq T (lift h d0 (TLRef n)) (TLRef (plus n h))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t))
(le d0 n)→(ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t)))
end of h2
by (lt_le_e . . . h1 h2)
we proved ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t))
∀c0:C
.∀d0:nat
.∀h:nat
.∀H3:(drop h d0 c0 c).(ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t)))
case ty3_abst : n:nat c:C d:C u:T H0:getl n c (CHead d (Bind Abst) u) t:T H1:ty3 g d u t ⇒
the thesis becomes
∀c0:C
.∀d0:nat
.∀h:nat
.∀H3:(drop h d0 c0 c).(ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u)))
(H2) by induction hypothesis we know ∀c0:C.∀d0:nat.∀h:nat.(drop h d0 c0 d)→(ty3 g c0 (lift h d0 u) (lift h d0 t))
assume c0: C
assume d0: nat
assume h: nat
suppose H3: drop h d0 c0 c
(h1)
suppose H4: lt n d0
(H5)
consider H4
we proved lt n d0
that is equivalent to le (S n) d0
by (le_S . . previous)
we proved le (S n) (S d0)
by (le_S_n . . previous)
we proved le n d0
by (drop_getl_trans_le . . previous . . . H3 . H0)
ex3_2
C
C
λe0:C.λ:C.drop n O c0 e0
λe0:C.λe1:C.drop h (minus d0 n) e0 e1
λ:C.λe1:C.clear e1 (CHead d (Bind Abst) u)
end of H5
we proceed by induction on H5 to prove ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))
case ex3_2_intro : x0:C x1:C H6:drop n O c0 x0 H7:drop h (minus d0 n) x0 x1 H8:clear x1 (CHead d (Bind Abst) u) ⇒
the thesis becomes ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))
(H9)
by (minus_x_Sy . . H4)
we proved eq nat (minus d0 n) (S (minus d0 (S n)))
we proceed by induction on the previous result to prove drop h (S (minus d0 (S n))) x0 x1
case refl_equal : ⇒
the thesis becomes the hypothesis H7
drop h (S (minus d0 (S n))) x0 x1
end of H9
(H10)
by (drop_clear_S . . . . H9 . . . H8)
ex2
C
λc1:C.clear x0 (CHead c1 (Bind Abst) (lift h (minus d0 (S n)) u))
λc1:C.drop h (minus d0 (S n)) c1 d
end of H10
we proceed by induction on H10 to prove ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))
case ex_intro2 : x:C H11:clear x0 (CHead x (Bind Abst) (lift h (minus d0 (S n)) u)) H12:drop h (minus d0 (S n)) x d ⇒
the thesis becomes ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))
(h1)
consider H4
we proved lt n d0
that is equivalent to le (S n) d0
by (le_plus_minus_r . . previous)
we proved eq nat (plus (S n) (minus d0 (S n))) d0
we proceed by induction on the previous result to prove ty3 g c0 (TLRef n) (lift h d0 (lift (S n) O u))
case refl_equal : ⇒
the thesis becomes
ty3
g
c0
TLRef n
lift h (plus (S n) (minus d0 (S n))) (lift (S n) O u)
(h1)
consider H4
we proved lt n d0
that is equivalent to le (S n) d0
by (le_plus_minus . . previous)
we proved eq nat d0 (plus (S n) (minus d0 (S n)))
we proceed by induction on the previous result to prove ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S n)) u))
case refl_equal : ⇒
the thesis becomes ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S n)) u))
(h1)
by (getl_intro . . . . H6 H11)
getl n c0 (CHead x (Bind Abst) (lift h (minus d0 (S n)) u))
end of h1
(h2)
by (H2 . . . H12)
ty3 g x (lift h (minus d0 (S n)) u) (lift h (minus d0 (S n)) t)
end of h2
by (ty3_abst . . . . . h1 . h2)
ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S n)) u))
ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S n)) u))
end of h1
(h2)
by (le_O_n .)
we proved le O (minus d0 (S n))
by (lift_d . . . . . previous)
eq
T
lift h (plus (S n) (minus d0 (S n))) (lift (S n) O u)
lift (S n) O (lift h (minus d0 (S n)) u)
end of h2
by (eq_ind_r . . . h1 . h2)
ty3
g
c0
TLRef n
lift h (plus (S n) (minus d0 (S n))) (lift (S n) O u)
ty3 g c0 (TLRef n) (lift h d0 (lift (S n) O u))
end of h1
(h2)
by (lift_lref_lt . . . H4)
eq T (lift h d0 (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))
ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))
we proved ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))
(lt n d0)→(ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u)))
end of h1
(h2)
suppose H4: le d0 n
(h1)
(h1)
by (refl_equal . .)
we proved eq nat (plus (S O) n) (plus (S O) n)
eq nat (S n) (plus (S O) n)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus n (S O)) (plus (S O) n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq nat (S n) (plus n (S O))
we proceed by induction on the previous result to prove ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O u))
case refl_equal : ⇒
the thesis becomes ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O u))
(h1)
(h1)
by (drop_getl_trans_ge . . . . . H3 . H0 H4)
we proved getl (plus n h) c0 (CHead d (Bind Abst) u)
by (ty3_abst . . . . . previous . H1)
we proved ty3 g c0 (TLRef (plus n h)) (lift (S (plus n h)) O u)
ty3 g c0 (TLRef (plus n h)) (lift (plus (S n) h) O u)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus h (S n)) (plus (S n) h)
end of h2
by (eq_ind_r . . . h1 . h2)
ty3 g c0 (TLRef (plus n h)) (lift (plus h (S n)) O u)
end of h1
(h2)
(h1)
by (le_S . . H4)
we proved le d0 (S n)
le d0 (plus O (S n))
end of h1
(h2) by (le_O_n .) we proved le O d0
by (lift_free . . . . . h1 h2)
eq T (lift h d0 (lift (S n) O u)) (lift (plus h (S n)) O u)
end of h2
by (eq_ind_r . . . h1 . h2)
ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O u))
ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O u))
end of h1
(h2)
by (lift_lref_ge . . . H4)
eq T (lift h d0 (TLRef n)) (TLRef (plus n h))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))
(le d0 n)→(ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u)))
end of h2
by (lt_le_e . . . h1 h2)
we proved ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))
∀c0:C
.∀d0:nat
.∀h:nat
.∀H3:(drop h d0 c0 c).(ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u)))
case ty3_bind : c:C u:T t:T :ty3 g c u t b:B t0:T t3:T :ty3 g (CHead c (Bind b) u) t0 t3 ⇒
the thesis becomes
∀c0:C
.∀d:nat
.∀h:nat
.∀H4:drop h d c0 c
.ty3
g
c0
lift h d (THead (Bind b) u t0)
lift h d (THead (Bind b) u t3)
(H1) by induction hypothesis we know ∀c0:C.∀d:nat.∀h:nat.(drop h d c0 c)→(ty3 g c0 (lift h d u) (lift h d t))
(H3) by induction hypothesis we know
∀c0:C
.∀d:nat
.∀h:nat
.(drop h d c0 (CHead c (Bind b) u))→(ty3 g c0 (lift h d t0) (lift h d t3))
assume c0: C
assume d: nat
assume h: nat
suppose H4: drop h d c0 c
(h1)
(h1)
(h1)
by (H1 . . . H4)
ty3 g c0 (lift h d u) (lift h d t)
end of h1
(h2)
by (drop_skip_bind . . . . H4 . .)
we proved
drop
h
S d
CHead c0 (Bind b) (lift h d u)
CHead c (Bind b) u
by (H3 . . . previous)
ty3
g
CHead c0 (Bind b) (lift h d u)
lift h (S d) t0
lift h (S d) t3
end of h2
by (ty3_bind . . . . h1 . . . h2)
we proved
ty3
g
c0
THead (Bind b) (lift h d u) (lift h (S d) t0)
THead (Bind b) (lift h d u) (lift h (S d) t3)
ty3
g
c0
THead (Bind b) (lift h d u) (lift h (s (Bind b) d) t0)
THead (Bind b) (lift h d u) (lift h (s (Bind b) d) t3)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Bind b) u t3)
THead (Bind b) (lift h d u) (lift h (s (Bind b) d) t3)
end of h2
by (eq_ind_r . . . h1 . h2)
ty3
g
c0
THead (Bind b) (lift h d u) (lift h (s (Bind b) d) t0)
lift h d (THead (Bind b) u t3)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Bind b) u t0)
THead (Bind b) (lift h d u) (lift h (s (Bind b) d) t0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
ty3
g
c0
lift h d (THead (Bind b) u t0)
lift h d (THead (Bind b) u t3)
∀c0:C
.∀d:nat
.∀h:nat
.∀H4:drop h d c0 c
.ty3
g
c0
lift h d (THead (Bind b) u t0)
lift h d (THead (Bind b) u t3)
case ty3_appl : c:C w:T u:T :ty3 g c w u v:T t:T :ty3 g c v (THead (Bind Abst) u t) ⇒
the thesis becomes
∀c0:C
.∀d:nat
.∀h:nat
.∀H4:drop h d c0 c
.ty3
g
c0
lift h d (THead (Flat Appl) w v)
lift h d (THead (Flat Appl) w (THead (Bind Abst) u t))
(H1) by induction hypothesis we know ∀c0:C.∀d:nat.∀h:nat.(drop h d c0 c)→(ty3 g c0 (lift h d w) (lift h d u))
(H3) by induction hypothesis we know
∀c0:C
.∀d:nat
.∀h:nat
.drop h d c0 c
→ty3 g c0 (lift h d v) (lift h d (THead (Bind Abst) u t))
assume c0: C
assume d: nat
assume h: nat
suppose H4: drop h d c0 c
(h1)
(h1)
(h1)
(h1)
by (H1 . . . H4)
ty3 g c0 (lift h d w) (lift h d u)
end of h1
(h2)
by (lift_bind . . . . .)
we proved
eq
T
lift h d (THead (Bind Abst) u t)
THead (Bind Abst) (lift h d u) (lift h (S d) t)
we proceed by induction on the previous result to prove
ty3
g
c0
lift h d v
THead (Bind Abst) (lift h d u) (lift h (S d) t)
case refl_equal : ⇒
the thesis becomes ty3 g c0 (lift h d v) (lift h d (THead (Bind Abst) u t))
by (H3 . . . H4)
ty3 g c0 (lift h d v) (lift h d (THead (Bind Abst) u t))
ty3
g
c0
lift h d v
THead (Bind Abst) (lift h d u) (lift h (S d) t)
end of h2
by (ty3_appl . . . . h1 . . h2)
we proved
ty3
g
c0
THead (Flat Appl) (lift h d w) (lift h d v)
THead
Flat Appl
lift h d w
THead (Bind Abst) (lift h d u) (lift h (S d) t)
ty3
g
c0
THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v)
THead
Flat Appl
lift h d w
THead
Bind Abst
lift h (s (Flat Appl) d) u
lift h (s (Bind Abst) (s (Flat Appl) d)) t
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h (s (Flat Appl) d) (THead (Bind Abst) u t)
THead
Bind Abst
lift h (s (Flat Appl) d) u
lift h (s (Bind Abst) (s (Flat Appl) d)) t
end of h2
by (eq_ind_r . . . h1 . h2)
ty3
g
c0
THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v)
THead
Flat Appl
lift h d w
lift h (s (Flat Appl) d) (THead (Bind Abst) u t)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Appl) w (THead (Bind Abst) u t))
THead
Flat Appl
lift h d w
lift h (s (Flat Appl) d) (THead (Bind Abst) u t)
end of h2
by (eq_ind_r . . . h1 . h2)
ty3
g
c0
THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v)
lift h d (THead (Flat Appl) w (THead (Bind Abst) u t))
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Appl) w v)
THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
ty3
g
c0
lift h d (THead (Flat Appl) w v)
lift h d (THead (Flat Appl) w (THead (Bind Abst) u t))
∀c0:C
.∀d:nat
.∀h:nat
.∀H4:drop h d c0 c
.ty3
g
c0
lift h d (THead (Flat Appl) w v)
lift h d (THead (Flat Appl) w (THead (Bind Abst) u t))
case ty3_cast : c:C t0:T t3:T :ty3 g c t0 t3 t4:T :ty3 g c t3 t4 ⇒
the thesis becomes
∀c0:C
.∀d:nat
.∀h:nat
.∀H4:drop h d c0 c
.ty3
g
c0
lift h d (THead (Flat Cast) t3 t0)
lift h d (THead (Flat Cast) t4 t3)
(H1) by induction hypothesis we know ∀c0:C.∀d:nat.∀h:nat.(drop h d c0 c)→(ty3 g c0 (lift h d t0) (lift h d t3))
(H3) by induction hypothesis we know ∀c0:C.∀d:nat.∀h:nat.(drop h d c0 c)→(ty3 g c0 (lift h d t3) (lift h d t4))
assume c0: C
assume d: nat
assume h: nat
suppose H4: drop h d c0 c
(h1)
(h1)
(h1)
consider H4
we proved drop h d c0 c
that is equivalent to drop h (s (Flat Cast) d) c0 c
by (H1 . . . previous)
ty3 g c0 (lift h (s (Flat Cast) d) t0) (lift h (s (Flat Cast) d) t3)
end of h1
(h2)
by (H3 . . . H4)
we proved ty3 g c0 (lift h d t3) (lift h d t4)
ty3 g c0 (lift h (s (Flat Cast) d) t3) (lift h d t4)
end of h2
by (ty3_cast . . . . h1 . h2)
we proved
ty3
g
c0
THead
Flat Cast
lift h (s (Flat Cast) d) t3
lift h (s (Flat Cast) d) t0
THead (Flat Cast) (lift h d t4) (lift h (s (Flat Cast) d) t3)
ty3
g
c0
THead (Flat Cast) (lift h d t3) (lift h (s (Flat Cast) d) t0)
THead (Flat Cast) (lift h d t4) (lift h (s (Flat Cast) d) t3)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Cast) t4 t3)
THead (Flat Cast) (lift h d t4) (lift h (s (Flat Cast) d) t3)
end of h2
by (eq_ind_r . . . h1 . h2)
ty3
g
c0
THead (Flat Cast) (lift h d t3) (lift h (s (Flat Cast) d) t0)
lift h d (THead (Flat Cast) t4 t3)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Cast) t3 t0)
THead (Flat Cast) (lift h d t3) (lift h (s (Flat Cast) d) t0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
ty3
g
c0
lift h d (THead (Flat Cast) t3 t0)
lift h d (THead (Flat Cast) t4 t3)
∀c0:C
.∀d:nat
.∀h:nat
.∀H4:drop h d c0 c
.ty3
g
c0
lift h d (THead (Flat Cast) t3 t0)
lift h d (THead (Flat Cast) t4 t3)
we proved ∀c0:C.∀d:nat.∀h:nat.(drop h d c0 e)→(ty3 g c0 (lift h d t1) (lift h d t2))
we proved
∀g:G
.∀e:C
.∀t1:T
.∀t2:T
.ty3 g e t1 t2
→∀c0:C.∀d:nat.∀h:nat.(drop h d c0 e)→(ty3 g c0 (lift h d t1) (lift h d t2))