DEFINITION ty3_inv_lref_nf2_pc3()
TYPE =
∀g:G
.∀c:C
.∀u1:T
.∀i:nat
.ty3 g c (TLRef i) u1
→(nf2 c (TLRef i)
→∀u2:T.(nf2 c u2)→(pc3 c u1 u2)→(ex T λu:T.eq T u2 (lift (S i) O u)))
BODY =
assume g: G
assume c: C
assume u1: T
assume i: nat
suppose H: ty3 g c (TLRef i) u1
assume y: T
suppose H0: ty3 g c y u1
we proceed by induction on H0 to prove
eq T y (TLRef i)
→(nf2 c y
→∀u2:T.(nf2 c u2)→(pc3 c u1 u2)→(ex T λu:T.eq T u2 (lift (S i) O u)))
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 i)).∀H7:(nf2 c0 u).∀u2:T.∀H8:(nf2 c0 u2).∀H9:(pc3 c0 t2 u2).(ex T λu0:T.eq T u2 (lift (S i) O u0))
() by induction hypothesis we know
eq T t2 (TLRef i)
→(nf2 c0 t2)→∀u2:T.(nf2 c0 u2)→(pc3 c0 t u2)→(ex T λu:T.eq T u2 (lift (S i) O u))
(H4) by induction hypothesis we know
eq T u (TLRef i)
→(nf2 c0 u)→∀u2:T.(nf2 c0 u2)→(pc3 c0 t1 u2)→(ex T λu0:T.eq T u2 (lift (S i) O u0))
suppose H6: eq T u (TLRef i)
suppose H7: nf2 c0 u
assume u2: T
suppose H8: nf2 c0 u2
suppose H9: pc3 c0 t2 u2
(H10)
we proceed by induction on H6 to prove nf2 c0 (TLRef i)
case refl_equal : ⇒
the thesis becomes the hypothesis H7
nf2 c0 (TLRef i)
end of H10
(H11)
we proceed by induction on H6 to prove
eq T (TLRef i) (TLRef i)
→(nf2 c0 (TLRef i)
→∀u3:T.(nf2 c0 u3)→(pc3 c0 t1 u3)→(ex T λu0:T.eq T u3 (lift (S i) O u0)))
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq T (TLRef i) (TLRef i)
→(nf2 c0 (TLRef i)
→∀u3:T.(nf2 c0 u3)→(pc3 c0 t1 u3)→(ex T λu0:T.eq T u3 (lift (S i) O u0)))
end of H11
(H_y)
by (refl_equal . .)
we proved eq T (TLRef i) (TLRef i)
by (H11 previous H10 . H8)
(pc3 c0 t1 u2)→(ex T λu0:T.eq T u2 (lift (S i) O u0))
end of H_y
by (pc3_t . . . H5 . H9)
we proved pc3 c0 t1 u2
by (H_y previous)
we proved ex T λu0:T.eq T u2 (lift (S i) O u0)
∀H6:(eq T u (TLRef i)).∀H7:(nf2 c0 u).∀u2:T.∀H8:(nf2 c0 u2).∀H9:(pc3 c0 t2 u2).(ex T λu0:T.eq T u2 (lift (S i) O u0))
case ty3_sort : c0:C m:nat ⇒
the thesis becomes
∀H1:eq T (TSort m) (TLRef i)
.nf2 c0 (TSort m)
→∀u2:T
.nf2 c0 u2
→(pc3 c0 (TSort (next g m)) u2)→(ex T λu:T.eq T u2 (lift (S i) O u))
suppose H1: eq T (TSort m) (TLRef i)
suppose : nf2 c0 (TSort m)
assume u2: T
suppose : nf2 c0 u2
suppose : pc3 c0 (TSort (next g m)) u2
(H5)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE TLRef i 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 i OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H5
consider H5
we proved
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove ex T λu:T.eq T u2 (lift (S i) O u)
we proved ex T λu:T.eq T u2 (lift (S i) O u)
∀H1:eq T (TSort m) (TLRef i)
.nf2 c0 (TSort m)
→∀u2:T
.nf2 c0 u2
→(pc3 c0 (TSort (next g m)) u2)→(ex T λu:T.eq T u2 (lift (S i) O u))
case ty3_abbr : n:nat c0:C d:C u:T H1:getl n c0 (CHead d (Bind Abbr) u) t:T :ty3 g d u t ⇒
the thesis becomes
∀H4:eq T (TLRef n) (TLRef i)
.∀H5:nf2 c0 (TLRef n)
.∀u2:T.(nf2 c0 u2)→∀H7:(pc3 c0 (lift (S n) O t) u2).(ex T λu0:T.eq T u2 (lift (S i) O u0))
() by induction hypothesis we know
eq T u (TLRef i)
→(nf2 d u
→∀u2:T.(nf2 d u2)→(pc3 d t u2)→(ex T λu0:T.eq T u2 (lift (S i) O u0)))
suppose H4: eq T (TLRef n) (TLRef i)
suppose H5: nf2 c0 (TLRef n)
assume u2: T
suppose : nf2 c0 u2
suppose H7: pc3 c0 (lift (S n) O t) u2
(H8)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:T.nat> CASE TLRef n OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n
<λ:T.nat> CASE TLRef i OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n (TLRef n)
λe:T.<λ:T.nat> CASE e OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n (TLRef i)
end of H8
(H10)
consider H8
we proved
eq
nat
<λ:T.nat> CASE TLRef n OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n
<λ:T.nat> CASE TLRef i OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n
that is equivalent to eq nat n i
we proceed by induction on the previous result to prove nf2 c0 (TLRef i)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
nf2 c0 (TLRef i)
end of H10
(H11)
consider H8
we proved
eq
nat
<λ:T.nat> CASE TLRef n OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n
<λ:T.nat> CASE TLRef i OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n
that is equivalent to eq nat n i
we proceed by induction on the previous result to prove getl i c0 (CHead d (Bind Abbr) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
getl i c0 (CHead d (Bind Abbr) u)
end of H11
by (nf2_gen_lref . . . . H11 H10 .)
we proved ex T λu0:T.eq T u2 (lift (S i) O u0)
∀H4:eq T (TLRef n) (TLRef i)
.∀H5:nf2 c0 (TLRef n)
.∀u2:T.(nf2 c0 u2)→∀H7:(pc3 c0 (lift (S n) O t) u2).(ex T λu0:T.eq T u2 (lift (S i) O u0))
case ty3_abst : n:nat c0:C d:C u:T H1:getl n c0 (CHead d (Bind Abst) u) t:T :ty3 g d u t ⇒
the thesis becomes
∀H4:eq T (TLRef n) (TLRef i)
.∀H5:nf2 c0 (TLRef n)
.∀u2:T.∀H6:(nf2 c0 u2).∀H7:(pc3 c0 (lift (S n) O u) u2).(ex T λu0:T.eq T u2 (lift (S i) O u0))
() by induction hypothesis we know
eq T u (TLRef i)
→(nf2 d u
→∀u2:T.(nf2 d u2)→(pc3 d t u2)→(ex T λu0:T.eq T u2 (lift (S i) O u0)))
suppose H4: eq T (TLRef n) (TLRef i)
suppose H5: nf2 c0 (TLRef n)
assume u2: T
suppose H6: nf2 c0 u2
suppose H7: pc3 c0 (lift (S n) O u) u2
(H8)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:T.nat> CASE TLRef n OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n
<λ:T.nat> CASE TLRef i OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n (TLRef n)
λe:T.<λ:T.nat> CASE e OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n (TLRef i)
end of H8
(H9)
consider H8
we proved
eq
nat
<λ:T.nat> CASE TLRef n OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n
<λ:T.nat> CASE TLRef i OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n
that is equivalent to eq nat n i
we proceed by induction on the previous result to prove pc3 c0 (lift (S i) O u) u2
case refl_equal : ⇒
the thesis becomes the hypothesis H7
pc3 c0 (lift (S i) O u) u2
end of H9
(H11)
consider H8
we proved
eq
nat
<λ:T.nat> CASE TLRef n OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n
<λ:T.nat> CASE TLRef i OF TSort ⇒n | TLRef n0⇒n0 | THead ⇒n
that is equivalent to eq nat n i
we proceed by induction on the previous result to prove getl i c0 (CHead d (Bind Abst) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
getl i c0 (CHead d (Bind Abst) u)
end of H11
(H_y)
by (pc3_nf2_unfold . . . H9 H6)
pr3 c0 (lift (S i) O u) u2
end of H_y
(H12)
by (getl_drop . . . . . H11)
we proved drop (S i) O c0 d
by (pr3_gen_lift . . . . . H_y . previous)
ex2 T λt2:T.eq T u2 (lift (S i) O t2) λt2:T.pr3 d u t2
end of H12
we proceed by induction on H12 to prove ex T λu0:T.eq T u2 (lift (S i) O u0)
case ex_intro2 : x:T H13:eq T u2 (lift (S i) O x) :pr3 d u x ⇒
the thesis becomes ex T λu0:T.eq T u2 (lift (S i) O u0)
by (refl_equal . .)
we proved eq T (lift (S i) O x) (lift (S i) O x)
by (ex_intro . . . previous)
we proved ex T λu0:T.eq T (lift (S i) O x) (lift (S i) O u0)
by (eq_ind_r . . . previous . H13)
ex T λu0:T.eq T u2 (lift (S i) O u0)
we proved ex T λu0:T.eq T u2 (lift (S i) O u0)
∀H4:eq T (TLRef n) (TLRef i)
.∀H5:nf2 c0 (TLRef n)
.∀u2:T.∀H6:(nf2 c0 u2).∀H7:(pc3 c0 (lift (S n) O u) u2).(ex T λu0:T.eq T u2 (lift (S i) O u0))
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 i)
.nf2 c0 (THead (Bind b) u t1)
→∀u2:T
.nf2 c0 u2
→(pc3 c0 (THead (Bind b) u t2) u2)→(ex T λu0:T.eq T u2 (lift (S i) O u0))
() by induction hypothesis we know
eq T u (TLRef i)
→(nf2 c0 u)→∀u2:T.(nf2 c0 u2)→(pc3 c0 t u2)→(ex T λu0:T.eq T u2 (lift (S i) O u0))
() by induction hypothesis we know
eq T t1 (TLRef i)
→(nf2 (CHead c0 (Bind b) u) t1
→∀u2:T
.nf2 (CHead c0 (Bind b) u) u2
→(pc3 (CHead c0 (Bind b) u) t2 u2)→(ex T λu0:T.eq T u2 (lift (S i) O u0)))
suppose H5: eq T (THead (Bind b) u t1) (TLRef i)
suppose : nf2 c0 (THead (Bind b) u t1)
assume u2: T
suppose : nf2 c0 u2
suppose : pc3 c0 (THead (Bind b) u t2) u2
(H9)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE TLRef i 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 i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H9
consider H9
we proved
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove ex T λu0:T.eq T u2 (lift (S i) O u0)
we proved ex T λu0:T.eq T u2 (lift (S i) O u0)
∀H5:eq T (THead (Bind b) u t1) (TLRef i)
.nf2 c0 (THead (Bind b) u t1)
→∀u2:T
.nf2 c0 u2
→(pc3 c0 (THead (Bind b) u t2) u2)→(ex T λu0:T.eq T u2 (lift (S i) O u0))
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 i)
.nf2 c0 (THead (Flat Appl) w v)
→∀u2:T
.nf2 c0 u2
→(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) u2
→ex T λu0:T.eq T u2 (lift (S i) O u0))
() by induction hypothesis we know
eq T w (TLRef i)
→(nf2 c0 w)→∀u2:T.(nf2 c0 u2)→(pc3 c0 u u2)→(ex T λu0:T.eq T u2 (lift (S i) O u0))
() by induction hypothesis we know
eq T v (TLRef i)
→(nf2 c0 v
→∀u2:T
.nf2 c0 u2
→(pc3 c0 (THead (Bind Abst) u t) u2)→(ex T λu0:T.eq T u2 (lift (S i) O u0)))
suppose H5: eq T (THead (Flat Appl) w v) (TLRef i)
suppose : nf2 c0 (THead (Flat Appl) w v)
assume u2: T
suppose : nf2 c0 u2
suppose : pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) u2
(H9)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE TLRef i 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 i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H9
consider H9
we proved
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove ex T λu0:T.eq T u2 (lift (S i) O u0)
we proved ex T λu0:T.eq T u2 (lift (S i) O u0)
∀H5:eq T (THead (Flat Appl) w v) (TLRef i)
.nf2 c0 (THead (Flat Appl) w v)
→∀u2:T
.nf2 c0 u2
→(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) u2
→ex T λu0:T.eq T u2 (lift (S i) O u0))
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 i)
.nf2 c0 (THead (Flat Cast) t2 t1)
→∀u2:T
.nf2 c0 u2
→(pc3 c0 (THead (Flat Cast) t0 t2) u2)→(ex T λu:T.eq T u2 (lift (S i) O u))
() by induction hypothesis we know
eq T t1 (TLRef i)
→(nf2 c0 t1)→∀u2:T.(nf2 c0 u2)→(pc3 c0 t2 u2)→(ex T λu:T.eq T u2 (lift (S i) O u))
() by induction hypothesis we know
eq T t2 (TLRef i)
→(nf2 c0 t2)→∀u2:T.(nf2 c0 u2)→(pc3 c0 t0 u2)→(ex T λu:T.eq T u2 (lift (S i) O u))
suppose H5: eq T (THead (Flat Cast) t2 t1) (TLRef i)
suppose : nf2 c0 (THead (Flat Cast) t2 t1)
assume u2: T
suppose : nf2 c0 u2
suppose : pc3 c0 (THead (Flat Cast) t0 t2) u2
(H9)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE TLRef i 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 i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H9
consider H9
we proved
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove ex T λu:T.eq T u2 (lift (S i) O u)
we proved ex T λu:T.eq T u2 (lift (S i) O u)
∀H5:eq T (THead (Flat Cast) t2 t1) (TLRef i)
.nf2 c0 (THead (Flat Cast) t2 t1)
→∀u2:T
.nf2 c0 u2
→(pc3 c0 (THead (Flat Cast) t0 t2) u2)→(ex T λu:T.eq T u2 (lift (S i) O u))
we proved
eq T y (TLRef i)
→(nf2 c y
→∀u2:T.(nf2 c u2)→(pc3 c u1 u2)→(ex T λu:T.eq T u2 (lift (S i) O u)))
we proved
∀y:T
.ty3 g c y u1
→(eq T y (TLRef i)
→(nf2 c y
→∀u2:T.(nf2 c u2)→(pc3 c u1 u2)→(ex T λu:T.eq T u2 (lift (S i) O u))))
by (insert_eq . . . . previous H)
we proved
nf2 c (TLRef i)
→∀u2:T.(nf2 c u2)→(pc3 c u1 u2)→(ex T λu:T.eq T u2 (lift (S i) O u))
we proved
∀g:G
.∀c:C
.∀u1:T
.∀i:nat
.ty3 g c (TLRef i) u1
→(nf2 c (TLRef i)
→∀u2:T.(nf2 c u2)→(pc3 c u1 u2)→(ex T λu:T.eq T u2 (lift (S i) O u)))