DEFINITION lift_inj()
TYPE =
∀x:T.∀t:T.∀h:nat.∀d:nat.(eq T (lift h d x) (lift h d t))→(eq T x t)
BODY =
assume x: T
we proceed by induction on x to prove ∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d x) (lift h d t0))→(eq T x t0)
case TSort : n:nat ⇒
the thesis becomes
∀t:T
.∀h:nat
.∀d:nat.∀H:(eq T (lift h d (TSort n)) (lift h d t)).(eq T (TSort n) t)
assume t: T
assume h: nat
assume d: nat
suppose H: eq T (lift h d (TSort n)) (lift h d t)
(H0)
by (lift_sort . . .)
we proved eq T (lift h d (TSort n)) (TSort n)
we proceed by induction on the previous result to prove eq T (TSort n) (lift h d t)
case refl_equal : ⇒
the thesis becomes the hypothesis H
eq T (TSort n) (lift h d t)
end of H0
by (lift_gen_sort . . . . H0)
we proved eq T t (TSort n)
by (sym_eq . . . previous)
we proved eq T (TSort n) t
∀t:T
.∀h:nat
.∀d:nat.∀H:(eq T (lift h d (TSort n)) (lift h d t)).(eq T (TSort n) t)
case TLRef : n:nat ⇒
the thesis becomes
∀t:T
.∀h:nat
.∀d:nat.∀H:(eq T (lift h d (TLRef n)) (lift h d t)).(eq T (TLRef n) t)
assume t: T
assume h: nat
assume d: nat
suppose H: eq T (lift h d (TLRef n)) (lift h d t)
(h1)
suppose H0: lt n d
(H1)
by (lift_lref_lt . . . H0)
we proved eq T (lift h d (TLRef n)) (TLRef n)
we proceed by induction on the previous result to prove eq T (TLRef n) (lift h d t)
case refl_equal : ⇒
the thesis becomes the hypothesis H
eq T (TLRef n) (lift h d t)
end of H1
by (le_n .)
we proved le d d
by (lt_le_trans . . . H0 previous)
we proved lt n d
by (lift_gen_lref_lt . . . previous . H1)
we proved eq T t (TLRef n)
by (sym_eq . . . previous)
we proved eq T (TLRef n) t
(lt n d)→(eq T (TLRef n) t)
end of h1
(h2)
suppose H0: le d n
(H1)
by (lift_lref_ge . . . H0)
we proved eq T (lift h d (TLRef n)) (TLRef (plus n h))
we proceed by induction on the previous result to prove eq T (TLRef (plus n h)) (lift h d t)
case refl_equal : ⇒
the thesis becomes the hypothesis H
eq T (TLRef (plus n h)) (lift h d t)
end of H1
by (lift_gen_lref_ge . . . H0 . H1)
we proved eq T t (TLRef n)
by (sym_eq . . . previous)
we proved eq T (TLRef n) t
(le d n)→(eq T (TLRef n) t)
end of h2
by (lt_le_e . . . h1 h2)
we proved eq T (TLRef n) t
∀t:T
.∀h:nat
.∀d:nat.∀H:(eq T (lift h d (TLRef n)) (lift h d t)).(eq T (TLRef n) t)
case THead ⇒
we need to prove
∀k:K
.∀t:T
.∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d t) (lift h d t0))→(eq T t t0)
→∀t0:T
.∀t1:T.∀h:nat.∀d:nat.(eq T (lift h d t0) (lift h d t1))→(eq T t0 t1)
→∀t1:T
.∀h:nat
.∀d:nat
.(eq T (lift h d (THead k t t0)) (lift h d t1))→(eq T (THead k t t0) t1)
assume k: K
we proceed by induction on k to prove
∀t:T
.∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d t) (lift h d t0))→(eq T t t0)
→∀t0:T
.∀t1:T.∀h:nat.∀d:nat.(eq T (lift h d t0) (lift h d t1))→(eq T t0 t1)
→∀t1:T
.∀h:nat
.∀d:nat
.(eq T (lift h d (THead k t t0)) (lift h d t1))→(eq T (THead k t t0) t1)
case Bind : b:B ⇒
the thesis becomes
∀t:T
.∀H:∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d t) (lift h d t0))→(eq T t t0)
.∀t0:T
.∀H0:∀t1:T.∀h:nat.∀d:nat.(eq T (lift h d t0) (lift h d t1))→(eq T t0 t1)
.∀t1:T
.∀h:nat
.∀d:nat
.∀H1:eq T (lift h d (THead (Bind b) t t0)) (lift h d t1)
.eq T (THead (Bind b) t t0) t1
assume t: T
suppose H: ∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d t) (lift h d t0))→(eq T t t0)
assume t0: T
suppose H0: ∀t1:T.∀h:nat.∀d:nat.(eq T (lift h d t0) (lift h d t1))→(eq T t0 t1)
assume t1: T
assume h: nat
assume d: nat
suppose H1: eq T (lift h d (THead (Bind b) t t0)) (lift h d t1)
(H2)
by (lift_bind . . . . .)
we proved
eq
T
lift h d (THead (Bind b) t t0)
THead (Bind b) (lift h d t) (lift h (S d) t0)
we proceed by induction on the previous result to prove eq T (THead (Bind b) (lift h d t) (lift h (S d) t0)) (lift h d t1)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
eq T (THead (Bind b) (lift h d t) (lift h (S d) t0)) (lift h d t1)
end of H2
by (lift_gen_bind . . . . . . H2)
we proved
ex3_2
T
T
λy:T.λz:T.eq T t1 (THead (Bind b) y z)
λy:T.λ:T.eq T (lift h d t) (lift h d y)
λ:T.λz:T.eq T (lift h (S d) t0) (lift h (S d) z)
we proceed by induction on the previous result to prove eq T (THead (Bind b) t t0) t1
case ex3_2_intro : x0:T x1:T H3:eq T t1 (THead (Bind b) x0 x1) H4:eq T (lift h d t) (lift h d x0) H5:eq T (lift h (S d) t0) (lift h (S d) x1) ⇒
the thesis becomes eq T (THead (Bind b) t t0) t1
(h1)
by (refl_equal . .)
eq K (Bind b) (Bind b)
end of h1
(h2) by (H . . . H4) we proved eq T t x0
(h3) by (H0 . . . H5) we proved eq T t0 x1
by (f_equal3 . . . . . . . . . . . h1 h2 h3)
we proved eq T (THead (Bind b) t t0) (THead (Bind b) x0 x1)
by (eq_ind_r . . . previous . H3)
eq T (THead (Bind b) t t0) t1
we proved eq T (THead (Bind b) t t0) t1
∀t:T
.∀H:∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d t) (lift h d t0))→(eq T t t0)
.∀t0:T
.∀H0:∀t1:T.∀h:nat.∀d:nat.(eq T (lift h d t0) (lift h d t1))→(eq T t0 t1)
.∀t1:T
.∀h:nat
.∀d:nat
.∀H1:eq T (lift h d (THead (Bind b) t t0)) (lift h d t1)
.eq T (THead (Bind b) t t0) t1
case Flat : f:F ⇒
the thesis becomes
∀t:T
.∀H:∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d t) (lift h d t0))→(eq T t t0)
.∀t0:T
.∀H0:∀t1:T.∀h:nat.∀d:nat.(eq T (lift h d t0) (lift h d t1))→(eq T t0 t1)
.∀t1:T
.∀h:nat
.∀d:nat
.∀H1:eq T (lift h d (THead (Flat f) t t0)) (lift h d t1)
.eq T (THead (Flat f) t t0) t1
assume t: T
suppose H: ∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d t) (lift h d t0))→(eq T t t0)
assume t0: T
suppose H0: ∀t1:T.∀h:nat.∀d:nat.(eq T (lift h d t0) (lift h d t1))→(eq T t0 t1)
assume t1: T
assume h: nat
assume d: nat
suppose H1: eq T (lift h d (THead (Flat f) t t0)) (lift h d t1)
(H2)
by (lift_flat . . . . .)
we proved
eq
T
lift h d (THead (Flat f) t t0)
THead (Flat f) (lift h d t) (lift h d t0)
we proceed by induction on the previous result to prove eq T (THead (Flat f) (lift h d t) (lift h d t0)) (lift h d t1)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
eq T (THead (Flat f) (lift h d t) (lift h d t0)) (lift h d t1)
end of H2
by (lift_gen_flat . . . . . . H2)
we proved
ex3_2
T
T
λy:T.λz:T.eq T t1 (THead (Flat f) y z)
λy:T.λ:T.eq T (lift h d t) (lift h d y)
λ:T.λz:T.eq T (lift h d t0) (lift h d z)
we proceed by induction on the previous result to prove eq T (THead (Flat f) t t0) t1
case ex3_2_intro : x0:T x1:T H3:eq T t1 (THead (Flat f) x0 x1) H4:eq T (lift h d t) (lift h d x0) H5:eq T (lift h d t0) (lift h d x1) ⇒
the thesis becomes eq T (THead (Flat f) t t0) t1
(h1)
by (refl_equal . .)
eq K (Flat f) (Flat f)
end of h1
(h2) by (H . . . H4) we proved eq T t x0
(h3) by (H0 . . . H5) we proved eq T t0 x1
by (f_equal3 . . . . . . . . . . . h1 h2 h3)
we proved eq T (THead (Flat f) t t0) (THead (Flat f) x0 x1)
by (eq_ind_r . . . previous . H3)
eq T (THead (Flat f) t t0) t1
we proved eq T (THead (Flat f) t t0) t1
∀t:T
.∀H:∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d t) (lift h d t0))→(eq T t t0)
.∀t0:T
.∀H0:∀t1:T.∀h:nat.∀d:nat.(eq T (lift h d t0) (lift h d t1))→(eq T t0 t1)
.∀t1:T
.∀h:nat
.∀d:nat
.∀H1:eq T (lift h d (THead (Flat f) t t0)) (lift h d t1)
.eq T (THead (Flat f) t t0) t1
we proved
∀t:T
.∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d t) (lift h d t0))→(eq T t t0)
→∀t0:T
.∀t1:T.∀h:nat.∀d:nat.(eq T (lift h d t0) (lift h d t1))→(eq T t0 t1)
→∀t1:T
.∀h:nat
.∀d:nat
.(eq T (lift h d (THead k t t0)) (lift h d t1))→(eq T (THead k t t0) t1)
∀k:K
.∀t:T
.∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d t) (lift h d t0))→(eq T t t0)
→∀t0:T
.∀t1:T.∀h:nat.∀d:nat.(eq T (lift h d t0) (lift h d t1))→(eq T t0 t1)
→∀t1:T
.∀h:nat
.∀d:nat
.(eq T (lift h d (THead k t t0)) (lift h d t1))→(eq T (THead k t t0) t1)
we proved ∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d x) (lift h d t0))→(eq T x t0)
we proved ∀x:T.∀t0:T.∀h:nat.∀d:nat.(eq T (lift h d x) (lift h d t0))→(eq T x t0)