DEFINITION lift_gen_sort()
TYPE =
∀h:nat
.∀d:nat
.∀n:nat.∀t:T.(eq T (TSort n) (lift h d t))→(eq T t (TSort n))
BODY =
assume h: nat
assume d: nat
assume n: nat
assume t: T
we proceed by induction on t to prove (eq T (TSort n) (lift h d t))→(eq T t (TSort n))
case TSort : n0:nat ⇒
the thesis becomes
∀H:eq T (TSort n) (lift h d (TSort n0))
.eq T (TSort n0) (TSort n)
suppose H: eq T (TSort n) (lift h d (TSort n0))
consider H
we proved eq T (TSort n) (lift h d (TSort n0))
that is equivalent to eq T (TSort n) (TSort n0)
by (sym_eq . . . previous)
we proved eq T (TSort n0) (TSort n)
∀H:eq T (TSort n) (lift h d (TSort n0))
.eq T (TSort n0) (TSort n)
case TLRef : n0:nat ⇒
the thesis becomes
∀H:eq T (TSort n) (lift h d (TLRef n0))
.eq T (TLRef n0) (TSort n)
suppose H: eq T (TSort n) (lift h d (TLRef n0))
(h1)
suppose : lt n0 d
(H1)
(H1)
we proceed by induction on H to prove
<λ:T.Prop>
CASE lift h d (TLRef n0) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE lift h d (TLRef n0) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H1
consider H1
we proved
<λ:T.Prop>
CASE lift h d (TLRef n0) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove lt n0 d
we proved lt n0 d
by (lift_lref_lt . . . previous)
we proved eq T (lift h d (TLRef n0)) (TLRef n0)
we proceed by induction on the previous result to prove eq T (TSort n) (TLRef n0)
case refl_equal : ⇒
the thesis becomes the hypothesis H
eq T (TSort n) (TLRef n0)
end of H1
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE TLRef n0 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE TLRef n0 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H2
consider H2
we proved
<λ:T.Prop>
CASE TLRef n0 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove eq T (TLRef n0) (TSort n)
we proved eq T (TLRef n0) (TSort n)
(lt n0 d)→(eq T (TLRef n0) (TSort n))
end of h1
(h2)
suppose : le d n0
(H1)
(H1)
we proceed by induction on H to prove
<λ:T.Prop>
CASE lift h d (TLRef n0) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE lift h d (TLRef n0) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H1
consider H1
we proved
<λ:T.Prop>
CASE lift h d (TLRef n0) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove le d n0
we proved le d n0
by (lift_lref_ge . . . previous)
we proved eq T (lift h d (TLRef n0)) (TLRef (plus n0 h))
we proceed by induction on the previous result to prove eq T (TSort n) (TLRef (plus n0 h))
case refl_equal : ⇒
the thesis becomes the hypothesis H
eq T (TSort n) (TLRef (plus n0 h))
end of H1
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE TLRef (plus n0 h) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE TLRef (plus n0 h) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H2
consider H2
we proved
<λ:T.Prop>
CASE TLRef (plus n0 h) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove eq T (TLRef n0) (TSort n)
we proved eq T (TLRef n0) (TSort n)
(le d n0)→(eq T (TLRef n0) (TSort n))
end of h2
by (lt_le_e . . . h1 h2)
we proved eq T (TLRef n0) (TSort n)
∀H:eq T (TSort n) (lift h d (TLRef n0))
.eq T (TLRef n0) (TSort n)
case THead : k:K t0:T t1:T ⇒
the thesis becomes
∀H1:eq T (TSort n) (lift h d (THead k t0 t1))
.eq T (THead k t0 t1) (TSort n)
() by induction hypothesis we know (eq T (TSort n) (lift h d t0))→(eq T t0 (TSort n))
() by induction hypothesis we know (eq T (TSort n) (lift h d t1))→(eq T t1 (TSort n))
suppose H1: eq T (TSort n) (lift h d (THead k t0 t1))
(H2)
by (lift_head . . . . .)
we proved
eq
T
lift h d (THead k t0 t1)
THead k (lift h d t0) (lift h (s k d) t1)
we proceed by induction on the previous result to prove eq T (TSort n) (THead k (lift h d t0) (lift h (s k d) t1))
case refl_equal : ⇒
the thesis becomes the hypothesis H1
eq T (TSort n) (THead k (lift h d t0) (lift h (s k d) t1))
end of H2
(H3)
we proceed by induction on H2 to prove
<λ:T.Prop>
CASE THead k (lift h d t0) (lift h (s k d) t1) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE THead k (lift h d t0) (lift h (s k d) t1) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H3
consider H3
we proved
<λ:T.Prop>
CASE THead k (lift h d t0) (lift h (s k d) t1) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove eq T (THead k t0 t1) (TSort n)
we proved eq T (THead k t0 t1) (TSort n)
∀H1:eq T (TSort n) (lift h d (THead k t0 t1))
.eq T (THead k t0 t1) (TSort n)
we proved (eq T (TSort n) (lift h d t))→(eq T t (TSort n))
we proved
∀h:nat
.∀d:nat
.∀n:nat.∀t:T.(eq T (TSort n) (lift h d t))→(eq T t (TSort n))