DEFINITION sty0_lift()
TYPE =
∀g:G
.∀e:C
.∀t1:T
.∀t2:T
.sty0 g e t1 t2
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sty0 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: sty0 g e t1 t2
we proceed by induction on H to prove ∀c0:C.∀h:nat.∀d:nat.(drop h d c0 e)→(sty0 g c0 (lift h d t1) (lift h d t2))
case sty0_sort : c:C n:nat ⇒
the thesis becomes
∀c0:C
.∀h:nat
.∀d:nat
.drop h d c0 c
→sty0 g c0 (lift h d (TSort n)) (lift h d (TSort (next g n)))
assume c0: C
assume h: nat
assume d: nat
suppose : drop h d c0 c
(h1)
(h1)
by (sty0_sort . . .)
sty0 g c0 (TSort n) (TSort (next g n))
end of h1
(h2)
by (lift_sort . . .)
eq T (lift h d (TSort (next g n))) (TSort (next g n))
end of h2
by (eq_ind_r . . . h1 . h2)
sty0 g c0 (TSort n) (lift h d (TSort (next g n)))
end of h1
(h2)
by (lift_sort . . .)
eq T (lift h d (TSort n)) (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved sty0 g c0 (lift h d (TSort n)) (lift h d (TSort (next g n)))
∀c0:C
.∀h:nat
.∀d:nat
.drop h d c0 c
→sty0 g c0 (lift h d (TSort n)) (lift h d (TSort (next g n)))
case sty0_abbr : c:C d:C v:T i:nat H0:getl i c (CHead d (Bind Abbr) v) w:T H1:sty0 g d v w ⇒
the thesis becomes
∀c0:C
.∀h:nat
.∀d0:nat.∀H3:(drop h d0 c0 c).(sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w)))
(H2) by induction hypothesis we know ∀c0:C.∀h:nat.∀d0:nat.(drop h d0 c0 d)→(sty0 g c0 (lift h d0 v) (lift h d0 w))
assume c0: C
assume h: nat
assume d0: nat
suppose H3: drop h d0 c0 c
(h1)
suppose H4: lt i d0
(H5)
consider H4
we proved lt i d0
that is equivalent to le (S i) d0
by (le_S . . previous)
we proved le (S i) (S d0)
by (le_S_n . . previous)
we proved le i d0
by (drop_getl_trans_le . . previous . . . H3 . H0)
ex3_2
C
C
λe0:C.λ:C.drop i O c0 e0
λe0:C.λe1:C.drop h (minus d0 i) e0 e1
λ:C.λe1:C.clear e1 (CHead d (Bind Abbr) v)
end of H5
we proceed by induction on H5 to prove sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w))
case ex3_2_intro : x0:C x1:C H6:drop i O c0 x0 H7:drop h (minus d0 i) x0 x1 H8:clear x1 (CHead d (Bind Abbr) v) ⇒
the thesis becomes sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w))
(H9)
by (minus_x_Sy . . H4)
we proved eq nat (minus d0 i) (S (minus d0 (S i)))
we proceed by induction on the previous result to prove drop h (S (minus d0 (S i))) x0 x1
case refl_equal : ⇒
the thesis becomes the hypothesis H7
drop h (S (minus d0 (S i))) 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 i)) v))
λc1:C.drop h (minus d0 (S i)) c1 d
end of H10
we proceed by induction on H10 to prove sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w))
case ex_intro2 : x:C H11:clear x0 (CHead x (Bind Abbr) (lift h (minus d0 (S i)) v)) H12:drop h (minus d0 (S i)) x d ⇒
the thesis becomes sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w))
(h1)
consider H4
we proved lt i d0
that is equivalent to le (S i) d0
by (le_plus_minus_r . . previous)
we proved eq nat (plus (S i) (minus d0 (S i))) d0
we proceed by induction on the previous result to prove sty0 g c0 (TLRef i) (lift h d0 (lift (S i) O w))
case refl_equal : ⇒
the thesis becomes
sty0
g
c0
TLRef i
lift h (plus (S i) (minus d0 (S i))) (lift (S i) O w)
(h1)
consider H4
we proved lt i d0
that is equivalent to le (S i) d0
by (le_plus_minus . . previous)
we proved eq nat d0 (plus (S i) (minus d0 (S i)))
we proceed by induction on the previous result to prove sty0 g c0 (TLRef i) (lift (S i) O (lift h (minus d0 (S i)) w))
case refl_equal : ⇒
the thesis becomes sty0 g c0 (TLRef i) (lift (S i) O (lift h (minus d0 (S i)) w))
(h1)
by (getl_intro . . . . H6 H11)
getl i c0 (CHead x (Bind Abbr) (lift h (minus d0 (S i)) v))
end of h1
(h2)
by (H2 . . . H12)
sty0 g x (lift h (minus d0 (S i)) v) (lift h (minus d0 (S i)) w)
end of h2
by (sty0_abbr . . . . . h1 . h2)
sty0 g c0 (TLRef i) (lift (S i) O (lift h (minus d0 (S i)) w))
sty0 g c0 (TLRef i) (lift (S i) O (lift h (minus d0 (S i)) w))
end of h1
(h2)
by (le_O_n .)
we proved le O (minus d0 (S i))
by (lift_d . . . . . previous)
eq
T
lift h (plus (S i) (minus d0 (S i))) (lift (S i) O w)
lift (S i) O (lift h (minus d0 (S i)) w)
end of h2
by (eq_ind_r . . . h1 . h2)
sty0
g
c0
TLRef i
lift h (plus (S i) (minus d0 (S i))) (lift (S i) O w)
sty0 g c0 (TLRef i) (lift h d0 (lift (S i) O w))
end of h1
(h2)
by (lift_lref_lt . . . H4)
eq T (lift h d0 (TLRef i)) (TLRef i)
end of h2
by (eq_ind_r . . . h1 . h2)
sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w))
sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w))
we proved sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w))
(lt i d0)→(sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w)))
end of h1
(h2)
suppose H4: le d0 i
(h1)
(h1)
by (refl_equal . .)
we proved eq nat (plus (S O) i) (plus (S O) i)
eq nat (S i) (plus (S O) i)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus i (S O)) (plus (S O) i)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq nat (S i) (plus i (S O))
we proceed by induction on the previous result to prove sty0 g c0 (TLRef (plus i h)) (lift h d0 (lift (S i) O w))
case refl_equal : ⇒
the thesis becomes sty0 g c0 (TLRef (plus i h)) (lift h d0 (lift (S i) O w))
(h1)
(h1)
by (drop_getl_trans_ge . . . . . H3 . H0 H4)
we proved getl (plus i h) c0 (CHead d (Bind Abbr) v)
by (sty0_abbr . . . . . previous . H1)
we proved sty0 g c0 (TLRef (plus i h)) (lift (S (plus i h)) O w)
sty0 g c0 (TLRef (plus i h)) (lift (plus (S i) h) O w)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus h (S i)) (plus (S i) h)
end of h2
by (eq_ind_r . . . h1 . h2)
sty0 g c0 (TLRef (plus i h)) (lift (plus h (S i)) O w)
end of h1
(h2)
(h1)
by (le_S . . H4)
we proved le d0 (S i)
le d0 (plus O (S i))
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 i) O w)) (lift (plus h (S i)) O w)
end of h2
by (eq_ind_r . . . h1 . h2)
sty0 g c0 (TLRef (plus i h)) (lift h d0 (lift (S i) O w))
sty0 g c0 (TLRef (plus i h)) (lift h d0 (lift (S i) O w))
end of h1
(h2)
by (lift_lref_ge . . . H4)
eq T (lift h d0 (TLRef i)) (TLRef (plus i h))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w))
(le d0 i)→(sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w)))
end of h2
by (lt_le_e . . . h1 h2)
we proved sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w))
∀c0:C
.∀h:nat
.∀d0:nat.∀H3:(drop h d0 c0 c).(sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w)))
case sty0_abst : c:C d:C v:T i:nat H0:getl i c (CHead d (Bind Abst) v) w:T H1:sty0 g d v w ⇒
the thesis becomes
∀c0:C
.∀h:nat
.∀d0:nat.∀H3:(drop h d0 c0 c).(sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v)))
(H2) by induction hypothesis we know ∀c0:C.∀h:nat.∀d0:nat.(drop h d0 c0 d)→(sty0 g c0 (lift h d0 v) (lift h d0 w))
assume c0: C
assume h: nat
assume d0: nat
suppose H3: drop h d0 c0 c
(h1)
suppose H4: lt i d0
(H5)
consider H4
we proved lt i d0
that is equivalent to le (S i) d0
by (le_S . . previous)
we proved le (S i) (S d0)
by (le_S_n . . previous)
we proved le i d0
by (drop_getl_trans_le . . previous . . . H3 . H0)
ex3_2
C
C
λe0:C.λ:C.drop i O c0 e0
λe0:C.λe1:C.drop h (minus d0 i) e0 e1
λ:C.λe1:C.clear e1 (CHead d (Bind Abst) v)
end of H5
we proceed by induction on H5 to prove sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))
case ex3_2_intro : x0:C x1:C H6:drop i O c0 x0 H7:drop h (minus d0 i) x0 x1 H8:clear x1 (CHead d (Bind Abst) v) ⇒
the thesis becomes sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))
(H9)
by (minus_x_Sy . . H4)
we proved eq nat (minus d0 i) (S (minus d0 (S i)))
we proceed by induction on the previous result to prove drop h (S (minus d0 (S i))) x0 x1
case refl_equal : ⇒
the thesis becomes the hypothesis H7
drop h (S (minus d0 (S i))) 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 i)) v))
λc1:C.drop h (minus d0 (S i)) c1 d
end of H10
we proceed by induction on H10 to prove sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))
case ex_intro2 : x:C H11:clear x0 (CHead x (Bind Abst) (lift h (minus d0 (S i)) v)) H12:drop h (minus d0 (S i)) x d ⇒
the thesis becomes sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))
(h1)
consider H4
we proved lt i d0
that is equivalent to le (S i) d0
by (le_plus_minus_r . . previous)
we proved eq nat (plus (S i) (minus d0 (S i))) d0
we proceed by induction on the previous result to prove sty0 g c0 (TLRef i) (lift h d0 (lift (S i) O v))
case refl_equal : ⇒
the thesis becomes
sty0
g
c0
TLRef i
lift h (plus (S i) (minus d0 (S i))) (lift (S i) O v)
(h1)
consider H4
we proved lt i d0
that is equivalent to le (S i) d0
by (le_plus_minus . . previous)
we proved eq nat d0 (plus (S i) (minus d0 (S i)))
we proceed by induction on the previous result to prove sty0 g c0 (TLRef i) (lift (S i) O (lift h (minus d0 (S i)) v))
case refl_equal : ⇒
the thesis becomes sty0 g c0 (TLRef i) (lift (S i) O (lift h (minus d0 (S i)) v))
(h1)
by (getl_intro . . . . H6 H11)
getl i c0 (CHead x (Bind Abst) (lift h (minus d0 (S i)) v))
end of h1
(h2)
by (H2 . . . H12)
sty0 g x (lift h (minus d0 (S i)) v) (lift h (minus d0 (S i)) w)
end of h2
by (sty0_abst . . . . . h1 . h2)
sty0 g c0 (TLRef i) (lift (S i) O (lift h (minus d0 (S i)) v))
sty0 g c0 (TLRef i) (lift (S i) O (lift h (minus d0 (S i)) v))
end of h1
(h2)
by (le_O_n .)
we proved le O (minus d0 (S i))
by (lift_d . . . . . previous)
eq
T
lift h (plus (S i) (minus d0 (S i))) (lift (S i) O v)
lift (S i) O (lift h (minus d0 (S i)) v)
end of h2
by (eq_ind_r . . . h1 . h2)
sty0
g
c0
TLRef i
lift h (plus (S i) (minus d0 (S i))) (lift (S i) O v)
sty0 g c0 (TLRef i) (lift h d0 (lift (S i) O v))
end of h1
(h2)
by (lift_lref_lt . . . H4)
eq T (lift h d0 (TLRef i)) (TLRef i)
end of h2
by (eq_ind_r . . . h1 . h2)
sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))
sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))
we proved sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))
(lt i d0)→(sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v)))
end of h1
(h2)
suppose H4: le d0 i
(h1)
(h1)
by (refl_equal . .)
we proved eq nat (plus (S O) i) (plus (S O) i)
eq nat (S i) (plus (S O) i)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus i (S O)) (plus (S O) i)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq nat (S i) (plus i (S O))
we proceed by induction on the previous result to prove sty0 g c0 (TLRef (plus i h)) (lift h d0 (lift (S i) O v))
case refl_equal : ⇒
the thesis becomes sty0 g c0 (TLRef (plus i h)) (lift h d0 (lift (S i) O v))
(h1)
(h1)
by (drop_getl_trans_ge . . . . . H3 . H0 H4)
we proved getl (plus i h) c0 (CHead d (Bind Abst) v)
by (sty0_abst . . . . . previous . H1)
we proved sty0 g c0 (TLRef (plus i h)) (lift (S (plus i h)) O v)
sty0 g c0 (TLRef (plus i h)) (lift (plus (S i) h) O v)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus h (S i)) (plus (S i) h)
end of h2
by (eq_ind_r . . . h1 . h2)
sty0 g c0 (TLRef (plus i h)) (lift (plus h (S i)) O v)
end of h1
(h2)
(h1)
by (le_S . . H4)
we proved le d0 (S i)
le d0 (plus O (S i))
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 i) O v)) (lift (plus h (S i)) O v)
end of h2
by (eq_ind_r . . . h1 . h2)
sty0 g c0 (TLRef (plus i h)) (lift h d0 (lift (S i) O v))
sty0 g c0 (TLRef (plus i h)) (lift h d0 (lift (S i) O v))
end of h1
(h2)
by (lift_lref_ge . . . H4)
eq T (lift h d0 (TLRef i)) (TLRef (plus i h))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))
(le d0 i)→(sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v)))
end of h2
by (lt_le_e . . . h1 h2)
we proved sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))
∀c0:C
.∀h:nat
.∀d0:nat.∀H3:(drop h d0 c0 c).(sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v)))
case sty0_bind : b:B c:C v:T t3:T t4:T :sty0 g (CHead c (Bind b) v) t3 t4 ⇒
the thesis becomes
∀c0:C
.∀h:nat
.∀d:nat
.∀H2:drop h d c0 c
.sty0
g
c0
lift h d (THead (Bind b) v t3)
lift h d (THead (Bind b) v t4)
(H1) by induction hypothesis we know
∀c0:C
.∀h:nat
.∀d:nat
.(drop h d c0 (CHead c (Bind b) v))→(sty0 g c0 (lift h d t3) (lift h d t4))
assume c0: C
assume h: nat
assume d: nat
suppose H2: drop h d c0 c
(h1)
(h1)
by (drop_skip_bind . . . . H2 . .)
we proved
drop
h
S d
CHead c0 (Bind b) (lift h d v)
CHead c (Bind b) v
by (H1 . . . previous)
we proved
sty0
g
CHead c0 (Bind b) (lift h d v)
lift h (S d) t3
lift h (S d) t4
by (sty0_bind . . . . . . previous)
we proved
sty0
g
c0
THead (Bind b) (lift h d v) (lift h (S d) t3)
THead (Bind b) (lift h d v) (lift h (S d) t4)
sty0
g
c0
THead (Bind b) (lift h d v) (lift h (s (Bind b) d) t3)
THead (Bind b) (lift h d v) (lift h (s (Bind b) d) t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Bind b) v t4)
THead (Bind b) (lift h d v) (lift h (s (Bind b) d) t4)
end of h2
by (eq_ind_r . . . h1 . h2)
sty0
g
c0
THead (Bind b) (lift h d v) (lift h (s (Bind b) d) t3)
lift h d (THead (Bind b) v t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Bind b) v t3)
THead (Bind b) (lift h d v) (lift h (s (Bind b) d) t3)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
sty0
g
c0
lift h d (THead (Bind b) v t3)
lift h d (THead (Bind b) v t4)
∀c0:C
.∀h:nat
.∀d:nat
.∀H2:drop h d c0 c
.sty0
g
c0
lift h d (THead (Bind b) v t3)
lift h d (THead (Bind b) v t4)
case sty0_appl : c:C v:T t3:T t4:T :sty0 g c t3 t4 ⇒
the thesis becomes
∀c0:C
.∀h:nat
.∀d:nat
.∀H2:drop h d c0 c
.sty0
g
c0
lift h d (THead (Flat Appl) v t3)
lift h d (THead (Flat Appl) v t4)
(H1) by induction hypothesis we know ∀c0:C.∀h:nat.∀d:nat.(drop h d c0 c)→(sty0 g c0 (lift h d t3) (lift h d t4))
assume c0: C
assume h: nat
assume d: nat
suppose H2: drop h d c0 c
(h1)
(h1)
consider H2
we proved drop h d c0 c
that is equivalent to drop h (s (Flat Appl) d) c0 c
by (H1 . . . previous)
we proved sty0 g c0 (lift h (s (Flat Appl) d) t3) (lift h (s (Flat Appl) d) t4)
by (sty0_appl . . . . . previous)
sty0
g
c0
THead (Flat Appl) (lift h d v) (lift h (s (Flat Appl) d) t3)
THead (Flat Appl) (lift h d v) (lift h (s (Flat Appl) d) t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Appl) v t4)
THead (Flat Appl) (lift h d v) (lift h (s (Flat Appl) d) t4)
end of h2
by (eq_ind_r . . . h1 . h2)
sty0
g
c0
THead (Flat Appl) (lift h d v) (lift h (s (Flat Appl) d) t3)
lift h d (THead (Flat Appl) v t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Appl) v t3)
THead (Flat Appl) (lift h d v) (lift h (s (Flat Appl) d) t3)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
sty0
g
c0
lift h d (THead (Flat Appl) v t3)
lift h d (THead (Flat Appl) v t4)
∀c0:C
.∀h:nat
.∀d:nat
.∀H2:drop h d c0 c
.sty0
g
c0
lift h d (THead (Flat Appl) v t3)
lift h d (THead (Flat Appl) v t4)
case sty0_cast : c:C v1:T v2:T :sty0 g c v1 v2 t3:T t4:T :sty0 g c t3 t4 ⇒
the thesis becomes
∀c0:C
.∀h:nat
.∀d:nat
.∀H4:drop h d c0 c
.sty0
g
c0
lift h d (THead (Flat Cast) v1 t3)
lift h d (THead (Flat Cast) v2 t4)
(H1) by induction hypothesis we know ∀c0:C.∀h:nat.∀d:nat.(drop h d c0 c)→(sty0 g c0 (lift h d v1) (lift h d v2))
(H3) by induction hypothesis we know ∀c0:C.∀h:nat.∀d:nat.(drop h d c0 c)→(sty0 g c0 (lift h d t3) (lift h d t4))
assume c0: C
assume h: nat
assume d: nat
suppose H4: drop h d c0 c
(h1)
(h1)
(h1)
by (H1 . . . H4)
sty0 g c0 (lift h d v1) (lift h d v2)
end of h1
(h2)
consider H4
we proved drop h d c0 c
that is equivalent to drop h (s (Flat Cast) d) c0 c
by (H3 . . . previous)
sty0 g c0 (lift h (s (Flat Cast) d) t3) (lift h (s (Flat Cast) d) t4)
end of h2
by (sty0_cast . . . . h1 . . h2)
sty0
g
c0
THead (Flat Cast) (lift h d v1) (lift h (s (Flat Cast) d) t3)
THead (Flat Cast) (lift h d v2) (lift h (s (Flat Cast) d) t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Cast) v2 t4)
THead (Flat Cast) (lift h d v2) (lift h (s (Flat Cast) d) t4)
end of h2
by (eq_ind_r . . . h1 . h2)
sty0
g
c0
THead (Flat Cast) (lift h d v1) (lift h (s (Flat Cast) d) t3)
lift h d (THead (Flat Cast) v2 t4)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Cast) v1 t3)
THead (Flat Cast) (lift h d v1) (lift h (s (Flat Cast) d) t3)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
sty0
g
c0
lift h d (THead (Flat Cast) v1 t3)
lift h d (THead (Flat Cast) v2 t4)
∀c0:C
.∀h:nat
.∀d:nat
.∀H4:drop h d c0 c
.sty0
g
c0
lift h d (THead (Flat Cast) v1 t3)
lift h d (THead (Flat Cast) v2 t4)
we proved ∀c0:C.∀h:nat.∀d:nat.(drop h d c0 e)→(sty0 g c0 (lift h d t1) (lift h d t2))
we proved
∀g:G
.∀e:C
.∀t1:T
.∀t2:T
.sty0 g e t1 t2
→∀c0:C.∀h:nat.∀d:nat.(drop h d c0 e)→(sty0 g c0 (lift h d t1) (lift h d t2))