DEFINITION lift_gen_lift()
TYPE =
∀t1:T
.∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.le d1 d2
→(eq T (lift h1 d1 t1) (lift h2 (plus d2 h1) x)
→ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T t1 (lift h2 d2 t2))
BODY =
assume t1: T
we proceed by induction on t1 to prove
∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.le d1 d2
→(eq T (lift h1 d1 t1) (lift h2 (plus d2 h1) x)
→ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T t1 (lift h2 d2 t2))
case TSort : n:nat ⇒
the thesis becomes
∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.le d1 d2
→∀H0:eq T (lift h1 d1 (TSort n)) (lift h2 (plus d2 h1) x)
.ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TSort n) (lift h2 d2 t2)
assume x: T
assume h1: nat
assume h2: nat
assume d1: nat
assume d2: nat
suppose : le d1 d2
suppose H0: eq T (lift h1 d1 (TSort n)) (lift h2 (plus d2 h1) x)
(H1)
by (lift_sort . . .)
we proved eq T (lift h1 d1 (TSort n)) (TSort n)
we proceed by induction on the previous result to prove eq T (TSort n) (lift h2 (plus d2 h1) x)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
eq T (TSort n) (lift h2 (plus d2 h1) x)
end of H1
(h1)
(h1)
(h1)
by (refl_equal . .)
eq T (TSort n) (TSort n)
end of h1
(h2)
by (lift_sort . . .)
eq T (lift h1 d1 (TSort n)) (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TSort n) (lift h1 d1 (TSort n))
end of h1
(h2)
(h1)
by (refl_equal . .)
eq T (TSort n) (TSort n)
end of h1
(h2)
by (lift_sort . . .)
eq T (lift h2 d2 (TSort n)) (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TSort n) (lift h2 d2 (TSort n))
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt2:T.eq T (TSort n) (lift h1 d1 t2) λt2:T.eq T (TSort n) (lift h2 d2 t2)
end of h1
(h2)
by (lift_gen_sort . . . . H1)
eq T x (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TSort n) (lift h2 d2 t2)
∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.le d1 d2
→∀H0:eq T (lift h1 d1 (TSort n)) (lift h2 (plus d2 h1) x)
.ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TSort n) (lift h2 d2 t2)
case TLRef : n:nat ⇒
the thesis becomes
∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.∀H:le d1 d2
.∀H0:eq T (lift h1 d1 (TLRef n)) (lift h2 (plus d2 h1) x)
.ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2)
assume x: T
assume h1: nat
assume h2: nat
assume d1: nat
assume d2: nat
suppose H: le d1 d2
suppose H0: eq T (lift h1 d1 (TLRef n)) (lift h2 (plus d2 h1) x)
(h1)
suppose H1: lt n d1
(H2)
by (lift_lref_lt . . . H1)
we proved eq T (lift h1 d1 (TLRef n)) (TLRef n)
we proceed by induction on the previous result to prove eq T (TLRef n) (lift h2 (plus d2 h1) x)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
eq T (TLRef n) (lift h2 (plus d2 h1) x)
end of H2
(h1)
(h1)
(h1)
by (refl_equal . .)
eq T (TLRef n) (TLRef n)
end of h1
(h2)
by (lift_lref_lt . . . H1)
eq T (lift h1 d1 (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef n) (lift h1 d1 (TLRef n))
end of h1
(h2)
(h1)
by (refl_equal . .)
eq T (TLRef n) (TLRef n)
end of h1
(h2)
by (lt_le_trans . . . H1 H)
we proved lt n d2
by (lift_lref_lt . . . previous)
eq T (lift h2 d2 (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef n) (lift h2 d2 (TLRef n))
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt2:T.eq T (TLRef n) (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2)
end of h1
(h2)
by (le_plus_trans . . . H)
we proved le d1 (plus d2 h1)
by (lt_le_trans . . . H1 previous)
we proved lt n (plus d2 h1)
by (lift_gen_lref_lt . . . previous . H2)
eq T x (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2)
(lt n d1)→(ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2))
end of h1
(h2)
suppose H1: le d1 n
(H2)
by (lift_lref_ge . . . H1)
we proved eq T (lift h1 d1 (TLRef n)) (TLRef (plus n h1))
we proceed by induction on the previous result to prove eq T (TLRef (plus n h1)) (lift h2 (plus d2 h1) x)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
eq T (TLRef (plus n h1)) (lift h2 (plus d2 h1) x)
end of H2
(h1)
suppose H3: lt n d2
(h1)
(h1)
(h1)
by (refl_equal . .)
eq T (TLRef (plus n h1)) (TLRef (plus n h1))
end of h1
(h2)
by (lift_lref_ge . . . H1)
eq T (lift h1 d1 (TLRef n)) (TLRef (plus n h1))
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef (plus n h1)) (lift h1 d1 (TLRef n))
end of h1
(h2)
(h1)
by (refl_equal . .)
eq T (TLRef n) (TLRef n)
end of h1
(h2)
by (lift_lref_lt . . . H3)
eq T (lift h2 d2 (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef n) (lift h2 d2 (TLRef n))
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt2:T.eq T (TLRef (plus n h1)) (lift h1 d1 t2)
λt2:T.eq T (TLRef n) (lift h2 d2 t2)
end of h1
(h2)
by (lt_reg_r . . . H3)
we proved lt (plus n h1) (plus d2 h1)
by (lift_gen_lref_lt . . . previous . H2)
eq T x (TLRef (plus n h1))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2)
(lt n d2)→(ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2))
end of h1
(h2)
suppose H3: le d2 n
(h1)
suppose H4: lt n (plus d2 h2)
(h1)
by (le_n .)
we proved le h1 h1
by (le_plus_plus . . . . H3 previous)
le (plus d2 h1) (plus n h1)
end of h1
(h2)
(h1)
by (lt_reg_r . . . H4)
lt (plus n h1) (plus (plus d2 h2) h1)
end of h1
(h2)
by (plus_permute_2_in_3 . . .)
eq nat (plus (plus d2 h1) h2) (plus (plus d2 h2) h1)
end of h2
by (eq_ind_r . . . h1 . h2)
lt (plus n h1) (plus (plus d2 h1) h2)
end of h2
by (lift_gen_lref_false . . . h1 h2 . H2 .)
we proved ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2)
lt n (plus d2 h2)
→ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2)
end of h1
(h2)
suppose H4: le (plus d2 h2) n
(H5)
by (le_plus_r . .)
we proved le h2 (plus d2 h2)
by (le_trans . . . previous H4)
we proved le h2 n
by (le_plus_trans . . . previous)
we proved le h2 (plus n h1)
by (le_plus_minus_sym . . previous)
we proved eq nat (plus n h1) (plus (minus (plus n h1) h2) h2)
we proceed by induction on the previous result to prove eq T (TLRef (plus (minus (plus n h1) h2) h2)) (lift h2 (plus d2 h1) x)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
eq T (TLRef (plus (minus (plus n h1) h2) h2)) (lift h2 (plus d2 h1) x)
end of H5
(h1)
(h1)
(h1)
(h1)
by (refl_equal . .)
eq T (TLRef (plus (minus n h2) h1)) (TLRef (plus (minus n h2) h1))
end of h1
(h2)
by (le_minus . . . H4)
we proved le d2 (minus n h2)
by (le_trans . . . H previous)
we proved le d1 (minus n h2)
by (lift_lref_ge . . . previous)
eq T (lift h1 d1 (TLRef (minus n h2))) (TLRef (plus (minus n h2) h1))
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef (plus (minus n h2) h1)) (lift h1 d1 (TLRef (minus n h2)))
end of h1
(h2)
by (le_plus_r . .)
we proved le h2 (plus d2 h2)
by (le_trans . . . previous H4)
we proved le h2 n
by (le_minus_plus . . previous .)
eq nat (minus (plus n h1) h2) (plus (minus n h2) h1)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef (minus (plus n h1) h2)) (lift h1 d1 (TLRef (minus n h2)))
end of h1
(h2)
(h1)
(h1)
(h1)
by (minus_plus_r . .)
we proved eq nat (minus (plus (minus n h2) h2) h2) (minus n h2)
by (sym_eq . . . previous)
eq nat (minus n h2) (minus (plus (minus n h2) h2) h2)
end of h1
(h2)
by (refl_equal . .)
eq nat h2 h2
end of h2
by (f_equal2 . . . . . . . . h1 h2)
we proved
eq nat (plus (minus n h2) h2) (plus (minus (plus (minus n h2) h2) h2) h2)
by (f_equal . . . . . previous)
eq
T
TLRef (plus (minus n h2) h2)
TLRef (plus (minus (plus (minus n h2) h2) h2) h2)
end of h1
(h2)
(h1)
by (le_minus . . . H4)
le d2 (minus n h2)
end of h1
(h2) by (le_n .) we proved le h2 h2
by (le_plus_plus . . . . h1 h2)
we proved le (plus d2 h2) (plus (minus n h2) h2)
by (le_minus . . . previous)
we proved le d2 (minus (plus (minus n h2) h2) h2)
by (lift_lref_ge . . . previous)
eq
T
lift h2 d2 (TLRef (minus (plus (minus n h2) h2) h2))
TLRef (plus (minus (plus (minus n h2) h2) h2) h2)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
TLRef (plus (minus n h2) h2)
lift h2 d2 (TLRef (minus (plus (minus n h2) h2) h2))
end of h1
(h2)
by (le_plus_r . .)
we proved le h2 (plus d2 h2)
by (le_trans . . . previous H4)
we proved le h2 n
by (le_plus_minus_sym . . previous)
eq nat n (plus (minus n h2) h2)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef n) (lift h2 d2 (TLRef (minus n h2)))
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt2:T.eq T (TLRef (minus (plus n h1) h2)) (lift h1 d1 t2)
λt2:T.eq T (TLRef n) (lift h2 d2 t2)
end of h1
(h2)
by (arith0 . . . H4 .)
we proved le (plus d2 h1) (minus (plus n h1) h2)
by (lift_gen_lref_ge . . . previous . H5)
eq T x (TLRef (minus (plus n h1) h2))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2)
le (plus d2 h2) n
→ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2)
end of h2
by (lt_le_e . . . h1 h2)
we proved ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2)
(le d2 n)→(ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2))
end of h2
by (lt_le_e . . . h1 h2)
we proved ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2)
(le d1 n)→(ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2))
end of h2
by (lt_le_e . . . h1 h2)
we proved ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2)
∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.∀H:le d1 d2
.∀H0:eq T (lift h1 d1 (TLRef n)) (lift h2 (plus d2 h1) x)
.ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (TLRef n) (lift h2 d2 t2)
case THead : k:K t:T t0:T ⇒
the thesis becomes
∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.∀H1:le d1 d2
.∀H2:eq T (lift h1 d1 (THead k t t0)) (lift h2 (plus d2 h1) x)
.ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (THead k t t0) (lift h2 d2 t2)
(H) by induction hypothesis we know
∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.le d1 d2
→(eq T (lift h1 d1 t) (lift h2 (plus d2 h1) x)
→ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T t (lift h2 d2 t2))
(H0) by induction hypothesis we know
∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.le d1 d2
→(eq T (lift h1 d1 t0) (lift h2 (plus d2 h1) x)
→ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T t0 (lift h2 d2 t2))
assume x: T
assume h1: nat
assume h2: nat
assume d1: nat
assume d2: nat
suppose H1: le d1 d2
suppose H2: eq T (lift h1 d1 (THead k t t0)) (lift h2 (plus d2 h1) x)
assume b: B
suppose H3: eq T (lift h1 d1 (THead (Bind b) t t0)) (lift h2 (plus d2 h1) x)
(H4)
by (lift_bind . . . . .)
we proved
eq
T
lift h1 d1 (THead (Bind b) t t0)
THead (Bind b) (lift h1 d1 t) (lift h1 (S d1) t0)
we proceed by induction on the previous result to prove
eq
T
THead (Bind b) (lift h1 d1 t) (lift h1 (S d1) t0)
lift h2 (plus d2 h1) x
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq
T
THead (Bind b) (lift h1 d1 t) (lift h1 (S d1) t0)
lift h2 (plus d2 h1) x
end of H4
by (lift_gen_bind . . . . . . H4)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x (THead (Bind b) y z)
λy:T.λ:T.eq T (lift h1 d1 t) (lift h2 (plus d2 h1) y)
λ:T.λz:T.eq T (lift h1 (S d1) t0) (lift h2 (S (plus d2 h1)) z)
we proceed by induction on the previous result to prove ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (THead (Bind b) t t0) (lift h2 d2 t2)
case ex3_2_intro : x0:T x1:T H5:eq T x (THead (Bind b) x0 x1) H6:eq T (lift h1 d1 t) (lift h2 (plus d2 h1) x0) H7:eq T (lift h1 (S d1) t0) (lift h2 (S (plus d2 h1)) x1) ⇒
the thesis becomes ex2 T λt3:T.eq T x (lift h1 d1 t3) λt3:T.eq T (THead (Bind b) t t0) (lift h2 d2 t3)
by (H . . . . . H1 H6)
we proved ex2 T λt2:T.eq T x0 (lift h1 d1 t2) λt2:T.eq T t (lift h2 d2 t2)
we proceed by induction on the previous result to prove
ex2
T
λt2:T.eq T (THead (Bind b) x0 x1) (lift h1 d1 t2)
λt2:T.eq T (THead (Bind b) t t0) (lift h2 d2 t2)
case ex_intro2 : x2:T H8:eq T x0 (lift h1 d1 x2) H9:eq T t (lift h2 d2 x2) ⇒
the thesis becomes
ex2
T
λt3:T.eq T (THead (Bind b) x0 x1) (lift h1 d1 t3)
λt3:T.eq T (THead (Bind b) t t0) (lift h2 d2 t3)
(H10)
by (refl_equal . .)
eq nat (plus (S d2) h1) (plus (S d2) h1)
end of H10
(H11)
consider H10
we proved eq nat (plus (S d2) h1) (plus (S d2) h1)
that is equivalent to eq nat (S (plus d2 h1)) (plus (S d2) h1)
we proceed by induction on the previous result to prove eq T (lift h1 (S d1) t0) (lift h2 (plus (S d2) h1) x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H7
eq T (lift h1 (S d1) t0) (lift h2 (plus (S d2) h1) x1)
end of H11
by (le_n_S . . H1)
we proved le (S d1) (S d2)
by (H0 . . . . . previous H11)
we proved ex2 T λt2:T.eq T x1 (lift h1 (S d1) t2) λt2:T.eq T t0 (lift h2 (S d2) t2)
we proceed by induction on the previous result to prove
ex2
T
λt2:T.eq T (THead (Bind b) (lift h1 d1 x2) x1) (lift h1 d1 t2)
λt2:T.eq T (THead (Bind b) (lift h2 d2 x2) t0) (lift h2 d2 t2)
case ex_intro2 : x3:T H12:eq T x1 (lift h1 (S d1) x3) H13:eq T t0 (lift h2 (S d2) x3) ⇒
the thesis becomes
ex2
T
λt3:T.eq T (THead (Bind b) (lift h1 d1 x2) x1) (lift h1 d1 t3)
λt3:T.eq T (THead (Bind b) (lift h2 d2 x2) t0) (lift h2 d2 t3)
(h1)
(h1)
by (refl_equal . .)
eq
T
THead (Bind b) (lift h1 d1 x2) (lift h1 (S d1) x3)
THead (Bind b) (lift h1 d1 x2) (lift h1 (S d1) x3)
end of h1
(h2)
by (lift_bind . . . . .)
eq
T
lift h1 d1 (THead (Bind b) x2 x3)
THead (Bind b) (lift h1 d1 x2) (lift h1 (S d1) x3)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
THead (Bind b) (lift h1 d1 x2) (lift h1 (S d1) x3)
lift h1 d1 (THead (Bind b) x2 x3)
end of h1
(h2)
(h1)
by (refl_equal . .)
eq
T
THead (Bind b) (lift h2 d2 x2) (lift h2 (S d2) x3)
THead (Bind b) (lift h2 d2 x2) (lift h2 (S d2) x3)
end of h1
(h2)
by (lift_bind . . . . .)
eq
T
lift h2 d2 (THead (Bind b) x2 x3)
THead (Bind b) (lift h2 d2 x2) (lift h2 (S d2) x3)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
THead (Bind b) (lift h2 d2 x2) (lift h2 (S d2) x3)
lift h2 d2 (THead (Bind b) x2 x3)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T.eq T (THead (Bind b) (lift h1 d1 x2) (lift h1 (S d1) x3)) (lift h1 d1 t2)
λt2:T.eq T (THead (Bind b) (lift h2 d2 x2) (lift h2 (S d2) x3)) (lift h2 d2 t2)
by (eq_ind_r . . . previous . H13)
we proved
ex2
T
λt3:T.eq T (THead (Bind b) (lift h1 d1 x2) (lift h1 (S d1) x3)) (lift h1 d1 t3)
λt3:T.eq T (THead (Bind b) (lift h2 d2 x2) t0) (lift h2 d2 t3)
by (eq_ind_r . . . previous . H12)
ex2
T
λt3:T.eq T (THead (Bind b) (lift h1 d1 x2) x1) (lift h1 d1 t3)
λt3:T.eq T (THead (Bind b) (lift h2 d2 x2) t0) (lift h2 d2 t3)
we proved
ex2
T
λt2:T.eq T (THead (Bind b) (lift h1 d1 x2) x1) (lift h1 d1 t2)
λt2:T.eq T (THead (Bind b) (lift h2 d2 x2) t0) (lift h2 d2 t2)
by (eq_ind_r . . . previous . H9)
we proved
ex2
T
λt3:T.eq T (THead (Bind b) (lift h1 d1 x2) x1) (lift h1 d1 t3)
λt3:T.eq T (THead (Bind b) t t0) (lift h2 d2 t3)
by (eq_ind_r . . . previous . H8)
ex2
T
λt3:T.eq T (THead (Bind b) x0 x1) (lift h1 d1 t3)
λt3:T.eq T (THead (Bind b) t t0) (lift h2 d2 t3)
we proved
ex2
T
λt2:T.eq T (THead (Bind b) x0 x1) (lift h1 d1 t2)
λt2:T.eq T (THead (Bind b) t t0) (lift h2 d2 t2)
by (eq_ind_r . . . previous . H5)
ex2 T λt3:T.eq T x (lift h1 d1 t3) λt3:T.eq T (THead (Bind b) t t0) (lift h2 d2 t3)
we proved ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (THead (Bind b) t t0) (lift h2 d2 t2)
∀H3:eq T (lift h1 d1 (THead (Bind b) t t0)) (lift h2 (plus d2 h1) x)
.ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (THead (Bind b) t t0) (lift h2 d2 t2)
assume f: F
suppose H3: eq T (lift h1 d1 (THead (Flat f) t t0)) (lift h2 (plus d2 h1) x)
(H4)
by (lift_flat . . . . .)
we proved
eq
T
lift h1 d1 (THead (Flat f) t t0)
THead (Flat f) (lift h1 d1 t) (lift h1 d1 t0)
we proceed by induction on the previous result to prove eq T (THead (Flat f) (lift h1 d1 t) (lift h1 d1 t0)) (lift h2 (plus d2 h1) x)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq T (THead (Flat f) (lift h1 d1 t) (lift h1 d1 t0)) (lift h2 (plus d2 h1) x)
end of H4
by (lift_gen_flat . . . . . . H4)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x (THead (Flat f) y z)
λy:T.λ:T.eq T (lift h1 d1 t) (lift h2 (plus d2 h1) y)
λ:T.λz:T.eq T (lift h1 d1 t0) (lift h2 (plus d2 h1) z)
we proceed by induction on the previous result to prove ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (THead (Flat f) t t0) (lift h2 d2 t2)
case ex3_2_intro : x0:T x1:T H5:eq T x (THead (Flat f) x0 x1) H6:eq T (lift h1 d1 t) (lift h2 (plus d2 h1) x0) H7:eq T (lift h1 d1 t0) (lift h2 (plus d2 h1) x1) ⇒
the thesis becomes ex2 T λt3:T.eq T x (lift h1 d1 t3) λt3:T.eq T (THead (Flat f) t t0) (lift h2 d2 t3)
by (H . . . . . H1 H6)
we proved ex2 T λt2:T.eq T x0 (lift h1 d1 t2) λt2:T.eq T t (lift h2 d2 t2)
we proceed by induction on the previous result to prove
ex2
T
λt2:T.eq T (THead (Flat f) x0 x1) (lift h1 d1 t2)
λt2:T.eq T (THead (Flat f) t t0) (lift h2 d2 t2)
case ex_intro2 : x2:T H8:eq T x0 (lift h1 d1 x2) H9:eq T t (lift h2 d2 x2) ⇒
the thesis becomes
ex2
T
λt3:T.eq T (THead (Flat f) x0 x1) (lift h1 d1 t3)
λt3:T.eq T (THead (Flat f) t t0) (lift h2 d2 t3)
by (H0 . . . . . H1 H7)
we proved ex2 T λt2:T.eq T x1 (lift h1 d1 t2) λt2:T.eq T t0 (lift h2 d2 t2)
we proceed by induction on the previous result to prove
ex2
T
λt2:T.eq T (THead (Flat f) (lift h1 d1 x2) x1) (lift h1 d1 t2)
λt2:T.eq T (THead (Flat f) (lift h2 d2 x2) t0) (lift h2 d2 t2)
case ex_intro2 : x3:T H10:eq T x1 (lift h1 d1 x3) H11:eq T t0 (lift h2 d2 x3) ⇒
the thesis becomes
ex2
T
λt3:T.eq T (THead (Flat f) (lift h1 d1 x2) x1) (lift h1 d1 t3)
λt3:T.eq T (THead (Flat f) (lift h2 d2 x2) t0) (lift h2 d2 t3)
(h1)
(h1)
by (refl_equal . .)
eq
T
THead (Flat f) (lift h1 d1 x2) (lift h1 d1 x3)
THead (Flat f) (lift h1 d1 x2) (lift h1 d1 x3)
end of h1
(h2)
by (lift_flat . . . . .)
eq
T
lift h1 d1 (THead (Flat f) x2 x3)
THead (Flat f) (lift h1 d1 x2) (lift h1 d1 x3)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
THead (Flat f) (lift h1 d1 x2) (lift h1 d1 x3)
lift h1 d1 (THead (Flat f) x2 x3)
end of h1
(h2)
(h1)
by (refl_equal . .)
eq
T
THead (Flat f) (lift h2 d2 x2) (lift h2 d2 x3)
THead (Flat f) (lift h2 d2 x2) (lift h2 d2 x3)
end of h1
(h2)
by (lift_flat . . . . .)
eq
T
lift h2 d2 (THead (Flat f) x2 x3)
THead (Flat f) (lift h2 d2 x2) (lift h2 d2 x3)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
THead (Flat f) (lift h2 d2 x2) (lift h2 d2 x3)
lift h2 d2 (THead (Flat f) x2 x3)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T.eq T (THead (Flat f) (lift h1 d1 x2) (lift h1 d1 x3)) (lift h1 d1 t2)
λt2:T.eq T (THead (Flat f) (lift h2 d2 x2) (lift h2 d2 x3)) (lift h2 d2 t2)
by (eq_ind_r . . . previous . H11)
we proved
ex2
T
λt3:T.eq T (THead (Flat f) (lift h1 d1 x2) (lift h1 d1 x3)) (lift h1 d1 t3)
λt3:T.eq T (THead (Flat f) (lift h2 d2 x2) t0) (lift h2 d2 t3)
by (eq_ind_r . . . previous . H10)
ex2
T
λt3:T.eq T (THead (Flat f) (lift h1 d1 x2) x1) (lift h1 d1 t3)
λt3:T.eq T (THead (Flat f) (lift h2 d2 x2) t0) (lift h2 d2 t3)
we proved
ex2
T
λt2:T.eq T (THead (Flat f) (lift h1 d1 x2) x1) (lift h1 d1 t2)
λt2:T.eq T (THead (Flat f) (lift h2 d2 x2) t0) (lift h2 d2 t2)
by (eq_ind_r . . . previous . H9)
we proved
ex2
T
λt3:T.eq T (THead (Flat f) (lift h1 d1 x2) x1) (lift h1 d1 t3)
λt3:T.eq T (THead (Flat f) t t0) (lift h2 d2 t3)
by (eq_ind_r . . . previous . H8)
ex2
T
λt3:T.eq T (THead (Flat f) x0 x1) (lift h1 d1 t3)
λt3:T.eq T (THead (Flat f) t t0) (lift h2 d2 t3)
we proved
ex2
T
λt2:T.eq T (THead (Flat f) x0 x1) (lift h1 d1 t2)
λt2:T.eq T (THead (Flat f) t t0) (lift h2 d2 t2)
by (eq_ind_r . . . previous . H5)
ex2 T λt3:T.eq T x (lift h1 d1 t3) λt3:T.eq T (THead (Flat f) t t0) (lift h2 d2 t3)
we proved ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (THead (Flat f) t t0) (lift h2 d2 t2)
∀H3:eq T (lift h1 d1 (THead (Flat f) t t0)) (lift h2 (plus d2 h1) x)
.ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (THead (Flat f) t t0) (lift h2 d2 t2)
by (previous . H2)
we proved ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (THead k t t0) (lift h2 d2 t2)
∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.∀H1:le d1 d2
.∀H2:eq T (lift h1 d1 (THead k t t0)) (lift h2 (plus d2 h1) x)
.ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T (THead k t t0) (lift h2 d2 t2)
we proved
∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.le d1 d2
→(eq T (lift h1 d1 t1) (lift h2 (plus d2 h1) x)
→ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T t1 (lift h2 d2 t2))
we proved
∀t1:T
.∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.le d1 d2
→(eq T (lift h1 d1 t1) (lift h2 (plus d2 h1) x)
→ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T t1 (lift h2 d2 t2))