DEFINITION ty3_nf2_inv_abst()
TYPE =
∀g:G
.∀c:C
.∀t:T
.∀w:T
.∀u:T
.ty3 g c t (THead (Bind Abst) w u)
→(nf2 c t
→(nf2 c w
→(ty3_nf2_inv_abst_premise c w u
→(ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v))))
BODY =
assume g: G
assume c: C
assume t: T
assume w: T
assume u: T
suppose H: ty3 g c t (THead (Bind Abst) w u)
suppose H0: nf2 c t
suppose H1: nf2 c w
suppose H2: ty3_nf2_inv_abst_premise c w u
(H_x)
by (ty3_nf2_inv_all . . . . H H0)
or3
ex3_2
T
T
λw:T.λu0:T.eq T t (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c w
λw:T.λu0:T.nf2 (CHead c (Bind Abst) w) u0
ex nat λn:nat.eq T t (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c ws
λ:TList.λi:nat.nf2 c (TLRef i)
end of H_x
(H3) consider H_x
we proceed by induction on H3 to prove
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
case or3_intro0 : H4:ex3_2 T T λw0:T.λu0:T.eq T t (THead (Bind Abst) w0 u0) λw0:T.λ:T.nf2 c w0 λw0:T.λu0:T.nf2 (CHead c (Bind Abst) w0) u0 ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
we proceed by induction on H4 to prove
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
case ex3_2_intro : x0:T x1:T H5:eq T t (THead (Bind Abst) x0 x1) H6:nf2 c x0 H7:nf2 (CHead c (Bind Abst) x0) x1 ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
(H8)
we proceed by induction on H5 to prove ty3 g c (THead (Bind Abst) x0 x1) (THead (Bind Abst) w u)
case refl_equal : ⇒
the thesis becomes the hypothesis H
ty3 g c (THead (Bind Abst) x0 x1) (THead (Bind Abst) w u)
end of H8
by (ty3_correct . . . . H8)
we proved ex T λt:T.ty3 g c (THead (Bind Abst) w u) t
we proceed by induction on the previous result to prove
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
case ex_intro : x:T H9:ty3 g c (THead (Bind Abst) w u) x ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
by (ty3_gen_bind . . . . . . H9)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c (THead (Bind Abst) w t2) x
λ:T.λt:T.ty3 g c w t
λt2:T.λ:T.ty3 g (CHead c (Bind Abst) w) u t2
we proceed by induction on the previous result to prove
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
case ex3_2_intro : x2:T x3:T :pc3 c (THead (Bind Abst) w x2) x H11:ty3 g c w x3 H12:ty3 g (CHead c (Bind Abst) w) u x2 ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
by (ty3_gen_bind . . . . . . H8)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c (THead (Bind Abst) x0 t2) (THead (Bind Abst) w u)
λ:T.λt:T.ty3 g c x0 t
λt2:T.λ:T.ty3 g (CHead c (Bind Abst) x0) x1 t2
we proceed by induction on the previous result to prove
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
case ex3_2_intro : x4:T x5:T H13:pc3 c (THead (Bind Abst) x0 x4) (THead (Bind Abst) w u) :ty3 g c x0 x5 H15:ty3 g (CHead c (Bind Abst) x0) x1 x4 ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
by (pc3_gen_abst . . . . . H13)
we proved land (pc3 c x0 w) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) x4 u)
we proceed by induction on the previous result to prove
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
case conj : H16:pc3 c x0 w H17:∀b:B.∀u0:T.(pc3 (CHead c (Bind b) u0) x4 u) ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
(H_y) by (pc3_nf2 . . . H16 H6 H1) we proved eq T x0 w
(H18)
we proceed by induction on H_y to prove ty3 g (CHead c (Bind Abst) w) x1 x4
case refl_equal : ⇒
the thesis becomes the hypothesis H15
ty3 g (CHead c (Bind Abst) w) x1 x4
end of H18
(H19)
we proceed by induction on H_y to prove nf2 (CHead c (Bind Abst) w) x1
case refl_equal : ⇒
the thesis becomes the hypothesis H7
nf2 (CHead c (Bind Abst) w) x1
end of H19
(h1)
by (refl_equal . .)
eq T (THead (Bind Abst) w x1) (THead (Bind Abst) w x1)
end of h1
(h2)
by (H17 . .)
we proved pc3 (CHead c (Bind Abst) w) x4 u
by (ty3_conv . . . . H12 . . H18 previous)
ty3 g (CHead c (Bind Abst) w) x1 u
end of h2
by (ex4_2_intro . . . . . . . . h1 H11 h2 H19)
we proved
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) w x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
by (eq_ind_r . . . previous . H_y)
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
we proved
ex4_2
T
T
λv:T.λ:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
by (eq_ind_r . . . previous . H5)
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
case or3_intro1 : H4:ex nat λn:nat.eq T t (TSort n) ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
we proceed by induction on H4 to prove
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
case ex_intro : x:nat H5:eq T t (TSort x) ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
(H6)
we proceed by induction on H5 to prove ty3 g c (TSort x) (THead (Bind Abst) w u)
case refl_equal : ⇒
the thesis becomes the hypothesis H
ty3 g c (TSort x) (THead (Bind Abst) w u)
end of H6
by (ty3_gen_sort . . . . H6)
we proved pc3 c (TSort (next g x)) (THead (Bind Abst) w u)
by (pc3_gen_sort_abst . . . . previous .)
we proved
ex4_2
T
T
λv:T.λ:T.eq T (TSort x) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
by (eq_ind_r . . . previous . H5)
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
case or3_intro2 : H4:ex3_2 TList nat λws:TList.λi:nat.eq T t (THeads (Flat Appl) ws (TLRef i)) λws:TList.λ:nat.nfs2 c ws λ:TList.λi:nat.nf2 c (TLRef i) ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
we proceed by induction on H4 to prove
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
case ex3_2_intro : x0:TList x1:nat H5:eq T t (THeads (Flat Appl) x0 (TLRef x1)) :nfs2 c x0 H7:nf2 c (TLRef x1) ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
(H8)
we proceed by induction on H5 to prove ty3 g c (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind Abst) w u)
case refl_equal : ⇒
the thesis becomes the hypothesis H
ty3 g c (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind Abst) w u)
end of H8
(H9) consider H2
(H10) consider H8
we proceed by induction on x0 to prove
∀x:T
.∀x2:T
.ty3 g c (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq T (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
case TNil : ⇒
the thesis becomes
∀x:T
.∀x2:T
.(ty3
g
c
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
assume x: T
assume x2: T
we must prove
(ty3
g
c
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
or equivalently
ty3 g c (TLRef x1) (THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
suppose H11: ty3 g c (TLRef x1) (THead (Bind Abst) x x2)
suppose H12: ty3_nf2_inv_abst_premise c x x2
by (ty3_gen_lref . . . . H11)
we proved
or
ex3_3
C
T
T
λ:C.λ:T.λt:T.pc3 c (lift (S x1) O t) (THead (Bind Abst) x x2)
λe:C.λu:T.λ:T.getl x1 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 x1) O u) (THead (Bind Abst) x x2)
λe:C.λu:T.λ:T.getl x1 c (CHead e (Bind Abst) u)
λe:C.λu:T.λt:T.ty3 g e u t
we proceed by induction on the previous result to prove
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
case or_introl : H13:ex3_3 C T T λ:C.λ:T.λt0:T.pc3 c (lift (S x1) O t0) (THead (Bind Abst) x x2) λe:C.λu0:T.λ:T.getl x1 c (CHead e (Bind Abbr) u0) λe:C.λu0:T.λt0:T.ty3 g e u0 t0 ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
we proceed by induction on H13 to prove
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
case ex3_3_intro : x3:C x4:T x5:T :pc3 c (lift (S x1) O x5) (THead (Bind Abst) x x2) H15:getl x1 c (CHead x3 (Bind Abbr) x4) :ty3 g x3 x4 x5 ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
by (nf2_gen_lref . . . . H15 H7 .)
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
case or_intror : H13:ex3_3 C T T λ:C.λu0:T.λ:T.pc3 c (lift (S x1) O u0) (THead (Bind Abst) x x2) λe:C.λu0:T.λ:T.getl x1 c (CHead e (Bind Abst) u0) λe:C.λu0:T.λt0:T.ty3 g e u0 t0 ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
we proceed by induction on H13 to prove
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
case ex3_3_intro : x3:C x4:T x5:T H14:pc3 c (lift (S x1) O x4) (THead (Bind Abst) x x2) H15:getl x1 c (CHead x3 (Bind Abst) x4) :ty3 g x3 x4 x5 ⇒
the thesis becomes
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
(H_x0)
consider H14
we proved pc3 c (lift (S x1) O x4) (THead (Bind Abst) x x2)
that is equivalent to
pc3
c
THeads (Flat Appl) TNil (lift (S x1) O x4)
THead (Bind Abst) x x2
by (H12 . . . H15 . previous)
False
end of H_x0
(H17) consider H_x0
we proceed by induction on H17 to prove
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
we proved
ex4_2
T
T
λv:T.λ:T.eq T (TLRef x1) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
that is equivalent to
ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
we proved
ty3 g c (TLRef x1) (THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
that is equivalent to
(ty3
g
c
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
∀x:T
.∀x2:T
.(ty3
g
c
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
case TCons : t0:T t1:TList ⇒
the thesis becomes
∀x:T
.∀x2:T
.(ty3
g
c
THeads (Flat Appl) (TCons t0 t1) (TLRef x1)
THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) (TCons t0 t1) (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
(H11) by induction hypothesis we know
∀x:T
.∀x2:T
.ty3 g c (THeads (Flat Appl) t1 (TLRef x1)) (THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq T (THeads (Flat Appl) t1 (TLRef x1)) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
assume x: T
assume x2: T
we must prove
(ty3
g
c
THeads (Flat Appl) (TCons t0 t1) (TLRef x1)
THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) (TCons t0 t1) (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
or equivalently
(ty3
g
c
THead (Flat Appl) t0 (THeads (Flat Appl) t1 (TLRef x1))
THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) (TCons t0 t1) (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
suppose H12:
ty3
g
c
THead (Flat Appl) t0 (THeads (Flat Appl) t1 (TLRef x1))
THead (Bind Abst) x x2
suppose H13: ty3_nf2_inv_abst_premise c x x2
by (ty3_gen_appl . . . . . H12)
we proved
ex3_2
T
T
λu:T
.λt:T
.pc3
c
THead (Flat Appl) t0 (THead (Bind Abst) u t)
THead (Bind Abst) x x2
λu:T
.λt:T
.ty3 g c (THeads (Flat Appl) t1 (TLRef x1)) (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c t0 u
we proceed by induction on the previous result to prove
ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) t1 (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
case ex3_2_intro : x3:T x4:T H14:pc3 c (THead (Flat Appl) t0 (THead (Bind Abst) x3 x4)) (THead (Bind Abst) x x2) H15:ty3 g c (THeads (Flat Appl) t1 (TLRef x1)) (THead (Bind Abst) x3 x4) :ty3 g c t0 x3 ⇒
the thesis becomes
ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) t1 (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
(H_y)
by (ty3_nf2_gen__ty3_nf2_inv_abst_aux . . . H13 . . . H14)
ty3_nf2_inv_abst_premise c x3 x4
end of H_y
(H_x0)
by (H11 . . H15 H_y)
ex4_2
T
T
λv:T
.λ:T.eq T (THeads (Flat Appl) t1 (TLRef x1)) (THead (Bind Abst) x3 v)
λ:T.λw0:T.ty3 g c x3 w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x3) v x4
λv:T.λ:T.nf2 (CHead c (Bind Abst) x3) v
end of H_x0
(H17) consider H_x0
we proceed by induction on H17 to prove
ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) t1 (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
case ex4_2_intro : x5:T x6:T H18:eq T (THeads (Flat Appl) t1 (TLRef x1)) (THead (Bind Abst) x3 x5) :ty3 g c x3 x6 :ty3 g (CHead c (Bind Abst) x3) x5 x4 :nf2 (CHead c (Bind Abst) x3) x5 ⇒
the thesis becomes
ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) t1 (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
suppose H22:
eq
T
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x3 x5
(H23)
consider H22
we proved
eq
T
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x3 x5
that is equivalent to eq T (TLRef x1) (THead (Bind Abst) x3 x5)
we proceed by induction on the previous result to prove
<λ:T.Prop>
CASE THead (Bind Abst) x3 x5 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef x1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef x1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Bind Abst) x3 x5 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H23
consider H23
we proved
<λ:T.Prop>
CASE THead (Bind Abst) x3 x5 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) TNil (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
we proved
ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) TNil (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
(eq
T
THeads (Flat Appl) TNil (TLRef x1)
THead (Bind Abst) x3 x5)
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) TNil (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v)
assume t2: T
assume t3: TList
suppose :
eq T (THeads (Flat Appl) t3 (TLRef x1)) (THead (Bind Abst) x3 x5)
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) t3 (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v)
suppose H22:
eq
T
THeads (Flat Appl) (TCons t2 t3) (TLRef x1)
THead (Bind Abst) x3 x5
(H23)
consider H22
we proved
eq
T
THeads (Flat Appl) (TCons t2 t3) (TLRef x1)
THead (Bind Abst) x3 x5
that is equivalent to
eq
T
THead (Flat Appl) t2 (THeads (Flat Appl) t3 (TLRef x1))
THead (Bind Abst) x3 x5
we proceed by induction on the previous result to prove
<λ:T.Prop>
CASE THead (Bind Abst) x3 x5 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) t2 (THeads (Flat Appl) t3 (TLRef x1)) 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) t2 (THeads (Flat Appl) t3 (TLRef x1)) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind Abst) x3 x5 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
end of H23
consider H23
we proved
<λ:T.Prop>
CASE THead (Bind Abst) x3 x5 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
ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) (TCons t2 t3) (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
we proved
ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) (TCons t2 t3) (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
∀H22:eq
T
THeads (Flat Appl) (TCons t2 t3) (TLRef x1)
THead (Bind Abst) x3 x5
.ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) (TCons t2 t3) (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
by (previous . H18)
ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) t1 (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) t1 (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
we proved
ex4_2
T
T
λv:T
.λ:T
.eq
T
THead (Flat Appl) t0 (THeads (Flat Appl) t1 (TLRef x1))
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
that is equivalent to
ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) (TCons t0 t1) (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v
we proved
(ty3
g
c
THead (Flat Appl) t0 (THeads (Flat Appl) t1 (TLRef x1))
THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) (TCons t0 t1) (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
that is equivalent to
(ty3
g
c
THeads (Flat Appl) (TCons t0 t1) (TLRef x1)
THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) (TCons t0 t1) (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
∀x:T
.∀x2:T
.(ty3
g
c
THeads (Flat Appl) (TCons t0 t1) (TLRef x1)
THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq
T
THeads (Flat Appl) (TCons t0 t1) (TLRef x1)
THead (Bind Abst) x v
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
we proved
∀x:T
.∀x2:T
.ty3 g c (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind Abst) x x2)
→(ty3_nf2_inv_abst_premise c x x2
→(ex4_2
T
T
λv:T
.λ:T
.eq T (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind Abst) x v)
λ:T.λw0:T.ty3 g c x w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) x) v x2
λv:T.λ:T.nf2 (CHead c (Bind Abst) x) v))
by (unintro . . . previous)
we proved
∀x:T
.ty3 g c (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind Abst) w x)
→(ty3_nf2_inv_abst_premise c w x
→(ex4_2
T
T
λv:T
.λ:T
.eq T (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v x
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v))
by (unintro . . . previous H10)
we proved
ty3_nf2_inv_abst_premise c w u
→(ex4_2
T
T
λv:T
.λ:T
.eq T (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v)
by (previous H9)
we proved
ex4_2
T
T
λv:T
.λ:T
.eq T (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
by (eq_ind_r . . . previous . H5)
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
we proved
ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v
we proved
∀g:G
.∀c:C
.∀t:T
.∀w:T
.∀u:T
.ty3 g c t (THead (Bind Abst) w u)
→(nf2 c t
→(nf2 c w
→(ty3_nf2_inv_abst_premise c w u
→(ex4_2
T
T
λv:T.λ:T.eq T t (THead (Bind Abst) w v)
λ:T.λw0:T.ty3 g c w w0
λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v))))