DEFINITION lift_gen_head()
TYPE =
∀k:K
.∀u:T
.∀t:T
.∀x:T
.∀h:nat
.∀d:nat
.eq T (THead k u t) (lift h d x)
→(ex3_2
T
T
λy:T.λz:T.eq T x (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z))
BODY =
assume k: K
assume u: T
assume t: T
assume x: T
we proceed by induction on x to prove
∀h:nat
.∀d:nat
.eq T (THead k u t) (lift h d x)
→(ex3_2
T
T
λy:T.λz:T.eq T x (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z))
case TSort : n:nat ⇒
the thesis becomes
∀h:nat
.∀d:nat
.∀H:eq T (THead k u t) (lift h d (TSort n))
.ex3_2
T
T
λy:T.λz:T.eq T (TSort n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
assume h: nat
assume d: nat
suppose H: eq T (THead k u t) (lift h d (TSort n))
(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 (THead k u t) (TSort n)
case refl_equal : ⇒
the thesis becomes the hypothesis H
eq T (THead k u t) (TSort n)
end of H0
(H1)
we proceed by induction on H0 to prove
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead k u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead k u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H1
consider H1
we proved
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
T
T
λy:T.λz:T.eq T (TSort n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
we proved
ex3_2
T
T
λy:T.λz:T.eq T (TSort n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
∀h:nat
.∀d:nat
.∀H:eq T (THead k u t) (lift h d (TSort n))
.ex3_2
T
T
λy:T.λz:T.eq T (TSort n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
case TLRef : n:nat ⇒
the thesis becomes
∀h:nat
.∀d:nat
.∀H:eq T (THead k u t) (lift h d (TLRef n))
.ex3_2
T
T
λy:T.λz:T.eq T (TLRef n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
assume h: nat
assume d: nat
suppose H: eq T (THead k u t) (lift h d (TLRef n))
(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 (THead k u t) (TLRef n)
case refl_equal : ⇒
the thesis becomes the hypothesis H
eq T (THead k u t) (TLRef n)
end of H1
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead k u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead k u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H2
consider H2
we proved
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
T
T
λy:T.λz:T.eq T (TLRef n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
we proved
ex3_2
T
T
λy:T.λz:T.eq T (TLRef n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
lt n d
→(ex3_2
T
T
λy:T.λz:T.eq T (TLRef n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z))
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 (THead k u t) (TLRef (plus n h))
case refl_equal : ⇒
the thesis becomes the hypothesis H
eq T (THead k u t) (TLRef (plus n h))
end of H1
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE TLRef (plus n h) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead k u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead k u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef (plus n h) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H2
consider H2
we proved
<λ:T.Prop>
CASE TLRef (plus n h) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
T
T
λy:T.λz:T.eq T (TLRef n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
we proved
ex3_2
T
T
λy:T.λz:T.eq T (TLRef n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
le d n
→(ex3_2
T
T
λy:T.λz:T.eq T (TLRef n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z))
end of h2
by (lt_le_e . . . h1 h2)
we proved
ex3_2
T
T
λy:T.λz:T.eq T (TLRef n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
∀h:nat
.∀d:nat
.∀H:eq T (THead k u t) (lift h d (TLRef n))
.ex3_2
T
T
λy:T.λz:T.eq T (TLRef n) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
case THead : k0:K t0:T t1:T ⇒
the thesis becomes
∀h:nat
.∀d:nat
.∀H1:eq T (THead k u t) (lift h d (THead k0 t0 t1))
.ex3_2
T
T
λy:T.λz:T.eq T (THead k0 t0 t1) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
(H) by induction hypothesis we know
∀h:nat
.∀d:nat
.eq T (THead k u t) (lift h d t0)
→(ex3_2
T
T
λy:T.λz:T.eq T t0 (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z))
(H0) by induction hypothesis we know
∀h:nat
.∀d:nat
.eq T (THead k u t) (lift h d t1)
→(ex3_2
T
T
λy:T.λz:T.eq T t1 (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z))
assume h: nat
assume d: nat
suppose H1: eq T (THead k u t) (lift h d (THead k0 t0 t1))
(H2)
by (lift_head . . . . .)
we proved eq T (lift h d (THead k0 t0 t1)) (THead k0 (lift h d t0) (lift h (s k0 d) t1))
we proceed by induction on the previous result to prove eq T (THead k u t) (THead k0 (lift h d t0) (lift h (s k0 d) t1))
case refl_equal : ⇒
the thesis becomes the hypothesis H1
eq T (THead k u t) (THead k0 (lift h d t0) (lift h (s k0 d) t1))
end of H2
(H3)
by (f_equal . . . . . H2)
we proved
eq
K
<λ:T.K> CASE THead k u t OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
<λ:T.K>
CASE THead k0 (lift h d t0) (lift h (s k0 d) t1) OF
TSort ⇒k
| TLRef ⇒k
| THead k1 ⇒k1
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1 (THead k u t)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
THead k0 (lift h d t0) (lift h (s k0 d) t1)
end of H3
(h1)
(H4)
by (f_equal . . . . . H2)
we proved
eq
T
<λ:T.T> CASE THead k u t OF TSort ⇒u | TLRef ⇒u | THead t2 ⇒t2
<λ:T.T>
CASE THead k0 (lift h d t0) (lift h (s k0 d) t1) OF
TSort ⇒u
| TLRef ⇒u
| THead t2 ⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u | TLRef ⇒u | THead t2 ⇒t2 (THead k u t)
λe:T.<λ:T.T> CASE e OF TSort ⇒u | TLRef ⇒u | THead t2 ⇒t2
THead k0 (lift h d t0) (lift h (s k0 d) t1)
end of H4
(h1)
(H5)
by (f_equal . . . . . H2)
we proved
eq
T
<λ:T.T> CASE THead k u t OF TSort ⇒t | TLRef ⇒t | THead t2⇒t2
<λ:T.T>
CASE THead k0 (lift h d t0) (lift h (s k0 d) t1) OF
TSort ⇒t
| TLRef ⇒t
| THead t2⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t2⇒t2 (THead k u t)
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t2⇒t2
THead k0 (lift h d t0) (lift h (s k0 d) t1)
end of H5
suppose H6: eq T u (lift h d t0)
suppose H7: eq K k k0
(H8)
consider H5
we proved
eq
T
<λ:T.T> CASE THead k u t OF TSort ⇒t | TLRef ⇒t | THead t2⇒t2
<λ:T.T>
CASE THead k0 (lift h d t0) (lift h (s k0 d) t1) OF
TSort ⇒t
| TLRef ⇒t
| THead t2⇒t2
that is equivalent to eq T t (lift h (s k0 d) t1)
by (eq_ind_r . . . previous . H7)
eq T t (lift h (s k d) t1)
end of H8
we proceed by induction on H7 to prove
ex3_2
T
T
λy:T.λz:T.eq T (THead k0 t0 t1) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy:T.λz:T.eq T (THead k t0 t1) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
(H9)
we proceed by induction on H8 to prove
∀h0:nat
.∀d0:nat
.eq T (THead k u (lift h (s k d) t1)) (lift h0 d0 t1)
→(ex3_2
T
T
λy:T.λz:T.eq T t1 (THead k y z)
λy:T.λ:T.eq T u (lift h0 d0 y)
λ:T.λz:T.eq T (lift h (s k d) t1) (lift h0 (s k d0) z))
case refl_equal : ⇒
the thesis becomes the hypothesis H0
∀h0:nat
.∀d0:nat
.eq T (THead k u (lift h (s k d) t1)) (lift h0 d0 t1)
→(ex3_2
T
T
λy:T.λz:T.eq T t1 (THead k y z)
λy:T.λ:T.eq T u (lift h0 d0 y)
λ:T.λz:T.eq T (lift h (s k d) t1) (lift h0 (s k d0) z))
end of H9
(H10)
we proceed by induction on H8 to prove
∀h0:nat
.∀d0:nat
.eq T (THead k u (lift h (s k d) t1)) (lift h0 d0 t0)
→(ex3_2
T
T
λy:T.λz:T.eq T t0 (THead k y z)
λy:T.λ:T.eq T u (lift h0 d0 y)
λ:T.λz:T.eq T (lift h (s k d) t1) (lift h0 (s k d0) z))
case refl_equal : ⇒
the thesis becomes the hypothesis H
∀h0:nat
.∀d0:nat
.eq T (THead k u (lift h (s k d) t1)) (lift h0 d0 t0)
→(ex3_2
T
T
λy:T.λz:T.eq T t0 (THead k y z)
λy:T.λ:T.eq T u (lift h0 d0 y)
λ:T.λz:T.eq T (lift h (s k d) t1) (lift h0 (s k d0) z))
end of H10
(h1)
by (refl_equal . .)
eq T (THead k t0 t1) (THead k t0 t1)
end of h1
(h2)
by (refl_equal . .)
eq T (lift h d t0) (lift h d t0)
end of h2
(h3)
by (refl_equal . .)
eq T (lift h (s k d) t1) (lift h (s k d) t1)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λy:T.λz:T.eq T (THead k t0 t1) (THead k y z)
λy:T.λ:T.eq T (lift h d t0) (lift h d y)
λ:T.λz:T.eq T (lift h (s k d) t1) (lift h (s k d) z)
by (eq_ind_r . . . previous . H6)
we proved
ex3_2
T
T
λy:T.λz:T.eq T (THead k t0 t1) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T (lift h (s k d) t1) (lift h (s k d) z)
by (eq_ind_r . . . previous . H8)
ex3_2
T
T
λy:T.λz:T.eq T (THead k t0 t1) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
we proved
ex3_2
T
T
λy:T.λz:T.eq T (THead k0 t0 t1) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
eq T u (lift h d t0)
→(eq K k k0
→(ex3_2
T
T
λy:T.λz:T.eq T (THead k0 t0 t1) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)))
end of h1
(h2)
consider H4
we proved
eq
T
<λ:T.T> CASE THead k u t OF TSort ⇒u | TLRef ⇒u | THead t2 ⇒t2
<λ:T.T>
CASE THead k0 (lift h d t0) (lift h (s k0 d) t1) OF
TSort ⇒u
| TLRef ⇒u
| THead t2 ⇒t2
eq T u (lift h d t0)
end of h2
by (h1 h2)
eq K k k0
→(ex3_2
T
T
λy:T.λz:T.eq T (THead k0 t0 t1) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z))
end of h1
(h2)
consider H3
we proved
eq
K
<λ:T.K> CASE THead k u t OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
<λ:T.K>
CASE THead k0 (lift h d t0) (lift h (s k0 d) t1) OF
TSort ⇒k
| TLRef ⇒k
| THead k1 ⇒k1
eq K k k0
end of h2
by (h1 h2)
we proved
ex3_2
T
T
λy:T.λz:T.eq T (THead k0 t0 t1) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
∀h:nat
.∀d:nat
.∀H1:eq T (THead k u t) (lift h d (THead k0 t0 t1))
.ex3_2
T
T
λy:T.λz:T.eq T (THead k0 t0 t1) (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z)
we proved
∀h:nat
.∀d:nat
.eq T (THead k u t) (lift h d x)
→(ex3_2
T
T
λy:T.λz:T.eq T x (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z))
we proved
∀k:K
.∀u:T
.∀t:T
.∀x:T
.∀h:nat
.∀d:nat
.eq T (THead k u t) (lift h d x)
→(ex3_2
T
T
λy:T.λz:T.eq T x (THead k y z)
λy:T.λ:T.eq T u (lift h d y)
λ:T.λz:T.eq T t (lift h (s k d) z))