DEFINITION ty3_gen_lref()
TYPE =
∀g:G
.∀c:C
.∀x:T
.∀n:nat
.ty3 g c (TLRef n) x
→(or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c (lift (S n) O t) x
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c (lift (S n) O u) x
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t)
BODY =
assume g: G
assume c: C
assume x: T
assume n: nat
suppose H: ty3 g c (TLRef n) x
assume y: T
suppose H0: ty3 g c y x
we proceed by induction on H0 to prove
eq T y (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt1:T.pc3 c (lift (S n) O t1) x
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
λe:C.λu:T.λt1:T.ty3 g e u t1
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c (lift (S n) O u) x
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
λe:C.λu:T.λt1:T.ty3 g e u t1)
case ty3_conv : c0:C t2:T t:T :ty3 g c0 t2 t u:T t1:T H3:ty3 g c0 u t1 H5:pc3 c0 t1 t2 ⇒
the thesis becomes
∀H6:eq T u (TLRef n)
.or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
() by induction hypothesis we know
eq T t2 (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt0:T.ty3 g e u t0
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) t
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt0:T.ty3 g e u t0)
(H4) by induction hypothesis we know
eq T u (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t1
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t1
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0)
suppose H6: eq T u (TLRef n)
(H7)
by (f_equal . . . . . H6)
we proved eq T u (TLRef n)
eq T (λe:T.e u) (λe:T.e (TLRef n))
end of H7
(H8)
we proceed by induction on H7 to prove
eq T (TLRef n) (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt3:T.pc3 c0 (lift (S n) O t3) t1
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt3:T.ty3 g e u0 t3
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t1
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt3:T.ty3 g e u0 t3)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq T (TLRef n) (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt3:T.pc3 c0 (lift (S n) O t3) t1
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt3:T.ty3 g e u0 t3
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t1
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt3:T.ty3 g e u0 t3)
end of H8
(H10)
by (refl_equal . .)
we proved eq T (TLRef n) (TLRef n)
by (H8 previous)
or
ex3_3
C
T
T
λ:C.λ:T.λt3:T.pc3 c0 (lift (S n) O t3) t1
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt3:T.ty3 g e u0 t3
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t1
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt3:T.ty3 g e u0 t3
end of H10
we proceed by induction on H10 to prove
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
case or_introl : H11:ex3_3 C T T λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t1 λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0) λe:C.λu0:T.λt0:T.ty3 g e u0 t0 ⇒
the thesis becomes
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
we proceed by induction on H11 to prove
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
case ex3_3_intro : x0:C x1:T x2:T H12:pc3 c0 (lift (S n) O x2) t1 H13:getl n c0 (CHead x0 (Bind Abbr) x1) H14:ty3 g x0 x1 x2 ⇒
the thesis becomes
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
by (pc3_t . . . H12 . H5)
we proved pc3 c0 (lift (S n) O x2) t2
by (ex3_3_intro . . . . . . . . . previous H13 H14)
we proved
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
by (or_introl . . previous)
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
case or_intror : H11:ex3_3 C T T λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t1 λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0) λe:C.λu0:T.λt0:T.ty3 g e u0 t0 ⇒
the thesis becomes
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
we proceed by induction on H11 to prove
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
case ex3_3_intro : x0:C x1:T x2:T H12:pc3 c0 (lift (S n) O x1) t1 H13:getl n c0 (CHead x0 (Bind Abst) x1) H14:ty3 g x0 x1 x2 ⇒
the thesis becomes
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
by (pc3_t . . . H12 . H5)
we proved pc3 c0 (lift (S n) O x1) t2
by (ex3_3_intro . . . . . . . . . previous H13 H14)
we proved
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
by (or_intror . . previous)
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
∀H6:eq T u (TLRef n)
.or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
case ty3_sort : c0:C m:nat ⇒
the thesis becomes
∀H1:eq T (TSort m) (TLRef n)
.or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) (TSort (next g m))
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) (TSort (next g m))
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t
suppose H1: eq T (TSort m) (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 m OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort m 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
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) (TSort (next g m))
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) (TSort (next g m))
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) (TSort (next g m))
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) (TSort (next g m))
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t
∀H1:eq T (TSort m) (TLRef n)
.or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) (TSort (next g m))
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) (TSort (next g m))
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t
case ty3_abbr : n0:nat c0:C d:C u:T H1:getl n0 c0 (CHead d (Bind Abbr) u) t:T H2:ty3 g d u t ⇒
the thesis becomes
∀H4:eq T (TLRef n0) (TLRef n)
.or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (lift (S n0) O t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (lift (S n0) O t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
() by induction hypothesis we know
eq T u (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 d (lift (S n) O t0) t
λe:C.λu0:T.λ:T.getl n d (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 d (lift (S n) O u0) t
λe:C.λu0:T.λ:T.getl n d (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0)
suppose H4: eq T (TLRef n0) (TLRef n)
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:T.nat> CASE TLRef n0 OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0
<λ:T.nat> CASE TLRef n OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0 (TLRef n0)
λe:T.<λ:T.nat> CASE e OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0 (TLRef n)
end of H5
(H6)
consider H5
we proved
eq
nat
<λ:T.nat> CASE TLRef n0 OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0
<λ:T.nat> CASE TLRef n OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0
that is equivalent to eq nat n0 n
we proceed by induction on the previous result to prove getl n c0 (CHead d (Bind Abbr) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
getl n c0 (CHead d (Bind Abbr) u)
end of H6
(h1)
by (pc3_refl . .)
we proved pc3 c0 (lift (S n) O t) (lift (S n) O t)
by (ex3_3_intro . . . . . . . . . previous H6 H2)
we proved
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (lift (S n) O t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
by (or_introl . . previous)
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (lift (S n) O t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (lift (S n) O t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
end of h1
(h2)
consider H5
we proved
eq
nat
<λ:T.nat> CASE TLRef n0 OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0
<λ:T.nat> CASE TLRef n OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0
eq nat n0 n
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (lift (S n0) O t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (lift (S n0) O t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
∀H4:eq T (TLRef n0) (TLRef n)
.or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (lift (S n0) O t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (lift (S n0) O t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
case ty3_abst : n0:nat c0:C d:C u:T H1:getl n0 c0 (CHead d (Bind Abst) u) t:T H2:ty3 g d u t ⇒
the thesis becomes
∀H4:eq T (TLRef n0) (TLRef n)
.or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (lift (S n0) O u)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (lift (S n0) O u)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
() by induction hypothesis we know
eq T u (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 d (lift (S n) O t0) t
λe:C.λu0:T.λ:T.getl n d (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 d (lift (S n) O u0) t
λe:C.λu0:T.λ:T.getl n d (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0)
suppose H4: eq T (TLRef n0) (TLRef n)
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:T.nat> CASE TLRef n0 OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0
<λ:T.nat> CASE TLRef n OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0 (TLRef n0)
λe:T.<λ:T.nat> CASE e OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0 (TLRef n)
end of H5
(H6)
consider H5
we proved
eq
nat
<λ:T.nat> CASE TLRef n0 OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0
<λ:T.nat> CASE TLRef n OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0
that is equivalent to eq nat n0 n
we proceed by induction on the previous result to prove getl n c0 (CHead d (Bind Abst) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
getl n c0 (CHead d (Bind Abst) u)
end of H6
(h1)
by (pc3_refl . .)
we proved pc3 c0 (lift (S n) O u) (lift (S n) O u)
by (ex3_3_intro . . . . . . . . . previous H6 H2)
we proved
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (lift (S n) O u)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
by (or_intror . . previous)
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (lift (S n) O u)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (lift (S n) O u)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
end of h1
(h2)
consider H5
we proved
eq
nat
<λ:T.nat> CASE TLRef n0 OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0
<λ:T.nat> CASE TLRef n OF TSort ⇒n0 | TLRef n1⇒n1 | THead ⇒n0
eq nat n0 n
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (lift (S n0) O u)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (lift (S n0) O u)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
∀H4:eq T (TLRef n0) (TLRef n)
.or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (lift (S n0) O u)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (lift (S n0) O u)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
case ty3_bind : c0:C u:T t:T :ty3 g c0 u t b:B t1:T t2:T :ty3 g (CHead c0 (Bind b) u) t1 t2 ⇒
the thesis becomes
∀H5:eq T (THead (Bind b) u t1) (TLRef n)
.or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (THead (Bind b) u t2)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (THead (Bind b) u t2)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
() by induction hypothesis we know
eq T u (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) t
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) t
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0)
() by induction hypothesis we know
eq T t1 (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 (CHead c0 (Bind b) u) (lift (S n) O t0) t2
λe:C.λu0:T.λ:T.getl n (CHead c0 (Bind b) u) (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 (CHead c0 (Bind b) u) (lift (S n) O u0) t2
λe:C.λu0:T.λ:T.getl n (CHead c0 (Bind b) u) (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0)
suppose H5: eq T (THead (Bind b) 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 (Bind b) u t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind b) 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
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (THead (Bind b) u t2)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (THead (Bind b) u t2)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (THead (Bind b) u t2)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (THead (Bind b) u t2)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
∀H5:eq T (THead (Bind b) u t1) (TLRef n)
.or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (THead (Bind b) u t2)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (THead (Bind b) u t2)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
case ty3_appl : c0:C w:T u:T :ty3 g c0 w u v:T t:T :ty3 g c0 v (THead (Bind Abst) u t) ⇒
the thesis becomes
∀H5:eq T (THead (Flat Appl) w v) (TLRef n)
.or
ex3_3
C
T
T
λ:C
.λ:T
.λt0:T
.pc3
c0
lift (S n) O t0
THead (Flat Appl) w (THead (Bind Abst) u t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C
.λu0:T
.λ:T
.pc3
c0
lift (S n) O u0
THead (Flat Appl) w (THead (Bind Abst) u t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
() by induction hypothesis we know
eq T w (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) u
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt:T.ty3 g e u0 t
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) u
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt:T.ty3 g e u0 t)
() by induction hypothesis we know
eq T v (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c0 (lift (S n) O t0) (THead (Bind Abst) u t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C.λu0:T.λ:T.pc3 c0 (lift (S n) O u0) (THead (Bind Abst) u t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0)
suppose H5: eq T (THead (Flat Appl) w v) (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) w v OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) w v 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
λ:C
.λ:T
.λt0:T
.pc3
c0
lift (S n) O t0
THead (Flat Appl) w (THead (Bind Abst) u t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C
.λu0:T
.λ:T
.pc3
c0
lift (S n) O u0
THead (Flat Appl) w (THead (Bind Abst) u t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
we proved
or
ex3_3
C
T
T
λ:C
.λ:T
.λt0:T
.pc3
c0
lift (S n) O t0
THead (Flat Appl) w (THead (Bind Abst) u t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C
.λu0:T
.λ:T
.pc3
c0
lift (S n) O u0
THead (Flat Appl) w (THead (Bind Abst) u t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
∀H5:eq T (THead (Flat Appl) w v) (TLRef n)
.or
ex3_3
C
T
T
λ:C
.λ:T
.λt0:T
.pc3
c0
lift (S n) O t0
THead (Flat Appl) w (THead (Bind Abst) u t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abbr) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
ex3_3
C
T
T
λ:C
.λu0:T
.λ:T
.pc3
c0
lift (S n) O u0
THead (Flat Appl) w (THead (Bind Abst) u t)
λe:C.λu0:T.λ:T.getl n c0 (CHead e (Bind Abst) u0)
λe:C.λu0:T.λt0:T.ty3 g e u0 t0
case ty3_cast : c0:C t1:T t2:T :ty3 g c0 t1 t2 t0:T :ty3 g c0 t2 t0 ⇒
the thesis becomes
∀H5:eq T (THead (Flat Cast) t2 t1) (TLRef n)
.or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) (THead (Flat Cast) t0 t2)
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) (THead (Flat Cast) t0 t2)
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t
() by induction hypothesis we know
eq T t1 (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) t2
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) t2
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t)
() by induction hypothesis we know
eq T t2 (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) t0
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) t0
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t)
suppose H5: eq T (THead (Flat Cast) t2 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) t2 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Cast) t2 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
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) (THead (Flat Cast) t0 t2)
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) (THead (Flat Cast) t0 t2)
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) (THead (Flat Cast) t0 t2)
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) (THead (Flat Cast) t0 t2)
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t
∀H5:eq T (THead (Flat Cast) t2 t1) (TLRef n)
.or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c0 (lift (S n) O t) (THead (Flat Cast) t0 t2)
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abbr) u)
λe:C.λu:T.λt:T.ty3 g e u t
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c0 (lift (S n) O u) (THead (Flat Cast) t0 t2)
λe:C.λu:T.λ:T.getl n c0 (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t
we proved
eq T y (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt1:T.pc3 c (lift (S n) O t1) x
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
λe:C.λu:T.λt1:T.ty3 g e u t1
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c (lift (S n) O u) x
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
λe:C.λu:T.λt1:T.ty3 g e u t1)
we proved
∀y:T
.ty3 g c y x
→(eq T y (TLRef n)
→(or
ex3_3
C
T
T
λ:C.λ:T.λt1:T.pc3 c (lift (S n) O t1) x
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
λe:C.λu:T.λt1:T.ty3 g e u t1
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c (lift (S n) O u) x
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
λe:C.λu:T.λt1:T.ty3 g e u t1))
by (insert_eq . . . . previous H)
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c (lift (S n) O t0) x
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
λe:C.λu:T.λt0:T.ty3 g e u t0
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c (lift (S n) O u) x
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
λe:C.λu:T.λt0:T.ty3 g e u t0
we proved
∀g:G
.∀c:C
.∀x:T
.∀n:nat
.ty3 g c (TLRef n) x
→(or
ex3_3
C
T
T
λ:C.λ:T.λt0:T.pc3 c (lift (S n) O t0) x
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
λe:C.λu:T.λt0:T.ty3 g e u t0
ex3_3
C
T
T
λ:C.λu:T.λ:T.pc3 c (lift (S n) O u) x
λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
λe:C.λu:T.λt0:T.ty3 g e u t0)