DEFINITION pr0_gen_lref()
TYPE =
∀x:T.∀n:nat.(pr0 (TLRef n) x)→(eq T x (TLRef n))
BODY =
assume x: T
assume n: nat
suppose H: pr0 (TLRef n) x
assume y: T
suppose H0: pr0 y x
we proceed by induction on H0 to prove (eq T y (TLRef n))→(eq T x y)
case pr0_refl : t:T ⇒
the thesis becomes ∀H1:(eq T t (TLRef n)).(eq T t t)
suppose H1: eq T t (TLRef n)
(H2)
by (f_equal . . . . . H1)
we proved eq T t (TLRef n)
eq T (λe:T.e t) (λe:T.e (TLRef n))
end of H2
by (refl_equal . .)
we proved eq T (TLRef n) (TLRef n)
by (eq_ind_r . . . previous . H2)
we proved eq T t t
∀H1:(eq T t (TLRef n)).(eq T t t)
case pr0_comp : u1:T u2:T :pr0 u1 u2 t1:T t2:T :pr0 t1 t2 k:K ⇒
the thesis becomes ∀H5:(eq T (THead k u1 t1) (TLRef n)).(eq T (THead k u2 t2) (THead k u1 t1))
() by induction hypothesis we know (eq T u1 (TLRef n))→(eq T u2 u1)
() by induction hypothesis we know (eq T t1 (TLRef n))→(eq T t2 t1)
suppose H5: eq T (THead k u1 t1) (TLRef n)
(H6)
we proceed by induction on H5 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 u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead k u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H6
consider H6
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 eq T (THead k u2 t2) (THead k u1 t1)
we proved eq T (THead k u2 t2) (THead k u1 t1)
∀H5:(eq T (THead k u1 t1) (TLRef n)).(eq T (THead k u2 t2) (THead k u1 t1))
case pr0_beta : u:T v1:T v2:T :pr0 v1 v2 t1:T t2:T :pr0 t1 t2 ⇒
the thesis becomes
∀H5:eq T (THead (Flat Appl) v1 (THead (Bind Abst) u t1)) (TLRef n)
.eq
T
THead (Bind Abbr) v2 t2
THead (Flat Appl) v1 (THead (Bind Abst) u t1)
() by induction hypothesis we know (eq T v1 (TLRef n))→(eq T v2 v1)
() by induction hypothesis we know (eq T t1 (TLRef n))→(eq T t2 t1)
suppose H5: eq T (THead (Flat Appl) v1 (THead (Bind Abst) u t1)) (TLRef n)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u t1) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind Abst) u t1) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H6
consider H6
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
eq
T
THead (Bind Abbr) v2 t2
THead (Flat Appl) v1 (THead (Bind Abst) u t1)
we proved
eq
T
THead (Bind Abbr) v2 t2
THead (Flat Appl) v1 (THead (Bind Abst) u t1)
∀H5:eq T (THead (Flat Appl) v1 (THead (Bind Abst) u t1)) (TLRef n)
.eq
T
THead (Bind Abbr) v2 t2
THead (Flat Appl) v1 (THead (Bind Abst) u t1)
case pr0_upsilon : b:B :not (eq B b Abst) v1:T v2:T :pr0 v1 v2 u1:T u2:T :pr0 u1 u2 t1:T t2:T :pr0 t1 t2 ⇒
the thesis becomes
∀H8:eq T (THead (Flat Appl) v1 (THead (Bind b) u1 t1)) (TLRef n)
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Flat Appl) v1 (THead (Bind b) u1 t1)
() by induction hypothesis we know (eq T v1 (TLRef n))→(eq T v2 v1)
() by induction hypothesis we know (eq T u1 (TLRef n))→(eq T u2 u1)
() by induction hypothesis we know (eq T t1 (TLRef n))→(eq T t2 t1)
suppose H8: eq T (THead (Flat Appl) v1 (THead (Bind b) u1 t1)) (TLRef n)
(H9)
we proceed by induction on H8 to prove
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t1) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) v1 (THead (Bind b) u1 t1) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H9
consider H9
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
eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Flat Appl) v1 (THead (Bind b) u1 t1)
we proved
eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Flat Appl) v1 (THead (Bind b) u1 t1)
∀H8:eq T (THead (Flat Appl) v1 (THead (Bind b) u1 t1)) (TLRef n)
.eq
T
THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)
THead (Flat Appl) v1 (THead (Bind b) u1 t1)
case pr0_delta : u1:T u2:T :pr0 u1 u2 t1:T t2:T :pr0 t1 t2 w:T :subst0 O u2 t2 w ⇒
the thesis becomes
∀H6:eq T (THead (Bind Abbr) u1 t1) (TLRef n)
.eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u1 t1)
() by induction hypothesis we know (eq T u1 (TLRef n))→(eq T u2 u1)
() by induction hypothesis we know (eq T t1 (TLRef n))→(eq T t2 t1)
suppose H6: eq T (THead (Bind Abbr) u1 t1) (TLRef n)
(H7)
we proceed by induction on H6 to prove
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind Abbr) u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind Abbr) u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H7
consider H7
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 eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u1 t1)
we proved eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u1 t1)
∀H6:eq T (THead (Bind Abbr) u1 t1) (TLRef n)
.eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u1 t1)
case pr0_zeta : b:B :not (eq B b Abst) t1:T t2:T :pr0 t1 t2 u:T ⇒
the thesis becomes
∀H4:eq T (THead (Bind b) u (lift (S O) O t1)) (TLRef n)
.eq T t2 (THead (Bind b) u (lift (S O) O t1))
() by induction hypothesis we know (eq T t1 (TLRef n))→(eq T t2 t1)
suppose H4: eq T (THead (Bind b) u (lift (S O) O t1)) (TLRef n)
(H5)
we proceed by induction on H4 to prove
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind b) u (lift (S O) O t1) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind b) u (lift (S O) O t1) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H5
consider H5
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 eq T t2 (THead (Bind b) u (lift (S O) O t1))
we proved eq T t2 (THead (Bind b) u (lift (S O) O t1))
∀H4:eq T (THead (Bind b) u (lift (S O) O t1)) (TLRef n)
.eq T t2 (THead (Bind b) u (lift (S O) O t1))
case pr0_tau : t1:T t2:T :pr0 t1 t2 u:T ⇒
the thesis becomes
∀H3:eq T (THead (Flat Cast) u t1) (TLRef n)
.eq T t2 (THead (Flat Cast) u t1)
() by induction hypothesis we know (eq T t1 (TLRef n))→(eq T t2 t1)
suppose H3: eq T (THead (Flat Cast) u t1) (TLRef n)
(H4)
we proceed by induction on H3 to prove
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Cast) u t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Cast) u t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H4
consider H4
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 eq T t2 (THead (Flat Cast) u t1)
we proved eq T t2 (THead (Flat Cast) u t1)
∀H3:eq T (THead (Flat Cast) u t1) (TLRef n)
.eq T t2 (THead (Flat Cast) u t1)
we proved (eq T y (TLRef n))→(eq T x y)
we proved ∀y:T.(pr0 y x)→(eq T y (TLRef n))→(eq T x y)
by (insert_eq . . . . previous H)
we proved eq T x (TLRef n)
we proved ∀x:T.∀n:nat.(pr0 (TLRef n) x)→(eq T x (TLRef n))