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