DEFINITION sty0_gen_lref()
TYPE =
∀g:G
.∀c:C
.∀x:T
.∀n:nat
.sty0 g c (TLRef n) x
→(or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T x (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T x (lift (S n) O u))
BODY =
assume g: G
assume c: C
assume x: T
assume n: nat
suppose H: sty0 g c (TLRef n) x
assume y: T
suppose H0: sty0 g c y x
we proceed by induction on H0 to prove
eq T y (TLRef n)
→(or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
λe:C.λu:T.λt1:T.sty0 g e u t1
λ:C.λ:T.λt1:T.eq T x (lift (S n) O t1)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
λe:C.λu:T.λt1:T.sty0 g e u t1
λ:C.λu:T.λ:T.eq T x (lift (S n) O u))
case sty0_sort : c0:C n0:nat ⇒
the thesis becomes
∀H1:eq T (TSort n0) (TLRef n)
.or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (TSort (next g n0)) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (TSort (next g n0)) (lift (S n) O u)
suppose H1: eq T (TSort n0) (TLRef n)
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n0 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n0 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H2
consider H2
we proved
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (TSort (next g n0)) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (TSort (next g n0)) (lift (S n) O u)
we proved
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (TSort (next g n0)) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (TSort (next g n0)) (lift (S n) O u)
∀H1:eq T (TSort n0) (TLRef n)
.or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (TSort (next g n0)) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (TSort (next g n0)) (lift (S n) O u)
case sty0_abbr : c0:C d:C v:T i:nat H1:getl i c0 (CHead d (Bind Abbr) v) w:T H2:sty0 g d v w ⇒
the thesis becomes
∀H4:eq T (TLRef i) (TLRef n)
.or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (lift (S i) O w) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (lift (S i) O w) (lift (S n) O u)
() by induction hypothesis we know
eq T v (TLRef n)
→(or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n d (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T w (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n d (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T w (lift (S n) O u))
suppose H4: eq T (TLRef i) (TLRef n)
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:T.nat> CASE TLRef i OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
<λ:T.nat> CASE TLRef n OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i (TLRef i)
λe:T.<λ:T.nat> CASE e OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i (TLRef n)
end of H5
(H6)
consider H5
we proved
eq
nat
<λ:T.nat> CASE TLRef i OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
<λ:T.nat> CASE TLRef n OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
that is equivalent to eq nat i n
we proceed by induction on the previous result to prove getl n c0 (CHead d (Bind Abbr) v)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
getl n c0 (CHead d (Bind Abbr) v)
end of H6
(h1)
by (refl_equal . .)
we proved eq T (lift (S n) O w) (lift (S n) O w)
by (ex3_3_intro . . . . . . . . . H6 H2 previous)
we proved
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (lift (S n) O w) (lift (S n) O t)
by (or_introl . . previous)
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (lift (S n) O w) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (lift (S n) O w) (lift (S n) O u)
end of h1
(h2)
consider H5
we proved
eq
nat
<λ:T.nat> CASE TLRef i OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
<λ:T.nat> CASE TLRef n OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
eq nat i n
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (lift (S i) O w) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (lift (S i) O w) (lift (S n) O u)
∀H4:eq T (TLRef i) (TLRef n)
.or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (lift (S i) O w) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (lift (S i) O w) (lift (S n) O u)
case sty0_abst : c0:C d:C v:T i:nat H1:getl i c0 (CHead d (Bind Abst) v) w:T H2:sty0 g d v w ⇒
the thesis becomes
∀H4:eq T (TLRef i) (TLRef n)
.or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (lift (S i) O v) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (lift (S i) O v) (lift (S n) O u)
() by induction hypothesis we know
eq T v (TLRef n)
→(or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n d (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T w (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n d (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T w (lift (S n) O u))
suppose H4: eq T (TLRef i) (TLRef n)
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:T.nat> CASE TLRef i OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
<λ:T.nat> CASE TLRef n OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i (TLRef i)
λe:T.<λ:T.nat> CASE e OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i (TLRef n)
end of H5
(H6)
consider H5
we proved
eq
nat
<λ:T.nat> CASE TLRef i OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
<λ:T.nat> CASE TLRef n OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
that is equivalent to eq nat i n
we proceed by induction on the previous result to prove getl n c0 (CHead d (Bind Abst) v)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
getl n c0 (CHead d (Bind Abst) v)
end of H6
(h1)
by (refl_equal . .)
we proved eq T (lift (S n) O v) (lift (S n) O v)
by (ex3_3_intro . . . . . . . . . H6 H2 previous)
we proved
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (lift (S n) O v) (lift (S n) O u)
by (or_intror . . previous)
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (lift (S n) O v) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (lift (S n) O v) (lift (S n) O u)
end of h1
(h2)
consider H5
we proved
eq
nat
<λ:T.nat> CASE TLRef i OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
<λ:T.nat> CASE TLRef n OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
eq nat i n
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (lift (S i) O v) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (lift (S i) O v) (lift (S n) O u)
∀H4:eq T (TLRef i) (TLRef n)
.or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (lift (S i) O v) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (lift (S i) O v) (lift (S n) O u)
case sty0_bind : b:B c0:C v:T t1:T t2:T :sty0 g (CHead c0 (Bind b) v) t1 t2 ⇒
the thesis becomes
∀H3:eq T (THead (Bind b) v t1) (TLRef n)
.or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (THead (Bind b) v t2) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (THead (Bind b) v t2) (lift (S n) O u)
() by induction hypothesis we know
eq T t1 (TLRef n)
→(or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n (CHead c0 (Bind b) v) (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T t2 (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n (CHead c0 (Bind b) v) (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T t2 (lift (S n) O u))
suppose H3: eq T (THead (Bind b) v 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 (Bind b) v t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind b) v 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
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (THead (Bind b) v t2) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (THead (Bind b) v t2) (lift (S n) O u)
we proved
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (THead (Bind b) v t2) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (THead (Bind b) v t2) (lift (S n) O u)
∀H3:eq T (THead (Bind b) v t1) (TLRef n)
.or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (THead (Bind b) v t2) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (THead (Bind b) v t2) (lift (S n) O u)
case sty0_appl : c0:C v:T t1:T t2:T :sty0 g c0 t1 t2 ⇒
the thesis becomes
∀H3:eq T (THead (Flat Appl) v t1) (TLRef n)
.or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (THead (Flat Appl) v t2) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (THead (Flat Appl) v t2) (lift (S n) O u)
() by induction hypothesis we know
eq T t1 (TLRef n)
→(or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T t2 (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T t2 (lift (S n) O u))
suppose H3: eq T (THead (Flat Appl) v 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 Appl) v t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) v 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
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (THead (Flat Appl) v t2) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (THead (Flat Appl) v t2) (lift (S n) O u)
we proved
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (THead (Flat Appl) v t2) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (THead (Flat Appl) v t2) (lift (S n) O u)
∀H3:eq T (THead (Flat Appl) v t1) (TLRef n)
.or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (THead (Flat Appl) v t2) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (THead (Flat Appl) v t2) (lift (S n) O u)
case sty0_cast : c0:C v1:T v2:T :sty0 g c0 v1 v2 t1:T t2:T :sty0 g c0 t1 t2 ⇒
the thesis becomes
∀H5:eq T (THead (Flat Cast) v1 t1) (TLRef n)
.or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (THead (Flat Cast) v2 t2) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (THead (Flat Cast) v2 t2) (lift (S n) O u)
() by induction hypothesis we know
eq T v1 (TLRef n)
→(or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T v2 (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T v2 (lift (S n) O u))
() by induction hypothesis we know
eq T t1 (TLRef n)
→(or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T t2 (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T t2 (lift (S n) O u))
suppose H5: eq T (THead (Flat Cast) v1 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 Cast) v1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Cast) v1 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
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (THead (Flat Cast) v2 t2) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (THead (Flat Cast) v2 t2) (lift (S n) O u)
we proved
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (THead (Flat Cast) v2 t2) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (THead (Flat Cast) v2 t2) (lift (S n) O u)
∀H5:eq T (THead (Flat Cast) v1 t1) (TLRef n)
.or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λ:T.λt:T.eq T (THead (Flat Cast) v2 t2) (lift (S n) O t)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.sty0 g e u t
λ:C.λu:T.λ:T.eq T (THead (Flat Cast) v2 t2) (lift (S n) O u)
we proved
eq T y (TLRef n)
→(or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
λe:C.λu:T.λt1:T.sty0 g e u t1
λ:C.λ:T.λt1:T.eq T x (lift (S n) O t1)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
λe:C.λu:T.λt1:T.sty0 g e u t1
λ:C.λu:T.λ:T.eq T x (lift (S n) O u))
we proved
∀y:T
.sty0 g c y x
→(eq T y (TLRef n)
→(or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
λe:C.λu:T.λt1:T.sty0 g e u t1
λ:C.λ:T.λt1:T.eq T x (lift (S n) O t1)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
λe:C.λu:T.λt1:T.sty0 g e u t1
λ:C.λu:T.λ:T.eq T x (lift (S n) O u)))
by (insert_eq . . . . previous H)
we proved
or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
λe:C.λu:T.λt0:T.sty0 g e u t0
λ:C.λ:T.λt0:T.eq T x (lift (S n) O t0)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
λe:C.λu:T.λt0:T.sty0 g e u t0
λ:C.λu:T.λ:T.eq T x (lift (S n) O u)
we proved
∀g:G
.∀c:C
.∀x:T
.∀n:nat
.sty0 g c (TLRef n) x
→(or
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
λe:C.λu:T.λt0:T.sty0 g e u t0
λ:C.λ:T.λt0:T.eq T x (lift (S n) O t0)
ex3_3
C
T
T
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
λe:C.λu:T.λt0:T.sty0 g e u t0
λ:C.λu:T.λ:T.eq T x (lift (S n) O u))