DEFINITION arity_nf2_inv_all()
TYPE =
∀g:G
.∀c:C
.∀t:T
.∀a:A
.arity g c t a
→(nf2 c t
→(or3
ex3_2
T
T
λw:T.λu:T.eq T t (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c w
λw:T.λu:T.nf2 (CHead c (Bind Abst) w) u
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)))
BODY =
assume g: G
assume c: C
assume t: T
assume a: A
suppose H: arity g c t a
we proceed by induction on H to prove
nf2 c t
→(or3
ex3_2
T
T
λw:T.λu:T.eq T t (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c w
λw:T.λu:T.nf2 (CHead c (Bind Abst) w) u
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))
case arity_sort : c0:C n:nat ⇒
the thesis becomes
nf2 c0 (TSort n)
→(or3
ex3_2
T
T
λw:T.λu:T.eq T (TSort n) (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn0:nat.eq T (TSort n) (TSort n0)
ex3_2
TList
nat
λws:TList
.λi:nat.eq T (TSort n) (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i))
suppose : nf2 c0 (TSort n)
by (refl_equal . .)
we proved eq T (TSort n) (TSort n)
by (ex_intro . . . previous)
we proved ex nat λn0:nat.eq T (TSort n) (TSort n0)
by (or3_intro1 . . . previous)
we proved
or3
ex3_2
T
T
λw:T.λu:T.eq T (TSort n) (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn0:nat.eq T (TSort n) (TSort n0)
ex3_2
TList
nat
λws:TList
.λi:nat.eq T (TSort n) (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
nf2 c0 (TSort n)
→(or3
ex3_2
T
T
λw:T.λu:T.eq T (TSort n) (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn0:nat.eq T (TSort n) (TSort n0)
ex3_2
TList
nat
λws:TList
.λi:nat.eq T (TSort n) (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i))
case arity_abbr : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u) a0:A :arity g d u a0 ⇒
the thesis becomes
∀H3:nf2 c0 (TLRef i)
.or3
ex3_2
T
T
λw:T.λu0:T.eq T (TLRef i) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (TLRef i) (TSort n)
ex3_2
TList
nat
λws:TList.λi0:nat.eq T (TLRef i) (THeads (Flat Appl) ws (TLRef i0))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi0:nat.nf2 c0 (TLRef i0)
() by induction hypothesis we know
nf2 d u
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T u (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 d w
λw:T.λu0:T.nf2 (CHead d (Bind Abst) w) u0
ex nat λn:nat.eq T u (TSort n)
ex3_2
TList
nat
λws:TList.λi0:nat.eq T u (THeads (Flat Appl) ws (TLRef i0))
λws:TList.λ:nat.nfs2 d ws
λ:TList.λi0:nat.nf2 d (TLRef i0))
suppose H3: nf2 c0 (TLRef i)
by (nf2_gen_lref . . . . H0 H3 .)
we proved
or3
ex3_2
T
T
λw:T.λu0:T.eq T (TLRef i) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (TLRef i) (TSort n)
ex3_2
TList
nat
λws:TList.λi0:nat.eq T (TLRef i) (THeads (Flat Appl) ws (TLRef i0))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi0:nat.nf2 c0 (TLRef i0)
∀H3:nf2 c0 (TLRef i)
.or3
ex3_2
T
T
λw:T.λu0:T.eq T (TLRef i) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (TLRef i) (TSort n)
ex3_2
TList
nat
λws:TList.λi0:nat.eq T (TLRef i) (THeads (Flat Appl) ws (TLRef i0))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi0:nat.nf2 c0 (TLRef i0)
case arity_abst : c0:C d:C u:T i:nat :getl i c0 (CHead d (Bind Abst) u) a0:A :arity g d u (asucc g a0) ⇒
the thesis becomes
∀H3:nf2 c0 (TLRef i)
.or3
ex3_2
T
T
λw:T.λu0:T.eq T (TLRef i) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (TLRef i) (TSort n)
ex3_2
TList
nat
λws:TList.λi0:nat.eq T (TLRef i) (THeads (Flat Appl) ws (TLRef i0))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi0:nat.nf2 c0 (TLRef i0)
() by induction hypothesis we know
nf2 d u
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T u (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 d w
λw:T.λu0:T.nf2 (CHead d (Bind Abst) w) u0
ex nat λn:nat.eq T u (TSort n)
ex3_2
TList
nat
λws:TList.λi0:nat.eq T u (THeads (Flat Appl) ws (TLRef i0))
λws:TList.λ:nat.nfs2 d ws
λ:TList.λi0:nat.nf2 d (TLRef i0))
suppose H3: nf2 c0 (TLRef i)
(h1)
by (refl_equal . .)
we proved eq T (TLRef i) (TLRef i)
eq T (TLRef i) (THeads (Flat Appl) TNil (TLRef i))
end of h1
(h2)
consider I
we proved True
nfs2 c0 TNil
end of h2
by (ex3_2_intro . . . . . . . h1 h2 H3)
we proved
ex3_2
TList
nat
λws:TList.λi0:nat.eq T (TLRef i) (THeads (Flat Appl) ws (TLRef i0))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi0:nat.nf2 c0 (TLRef i0)
by (or3_intro2 . . . previous)
we proved
or3
ex3_2
T
T
λw:T.λu0:T.eq T (TLRef i) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (TLRef i) (TSort n)
ex3_2
TList
nat
λws:TList.λi0:nat.eq T (TLRef i) (THeads (Flat Appl) ws (TLRef i0))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi0:nat.nf2 c0 (TLRef i0)
∀H3:nf2 c0 (TLRef i)
.or3
ex3_2
T
T
λw:T.λu0:T.eq T (TLRef i) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (TLRef i) (TSort n)
ex3_2
TList
nat
λws:TList.λi0:nat.eq T (TLRef i) (THeads (Flat Appl) ws (TLRef i0))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi0:nat.nf2 c0 (TLRef i0)
case arity_bind : b:B H0:not (eq B b Abst) c0:C u:T a1:A :arity g c0 u a1 t0:T a2:A H3:arity g (CHead c0 (Bind b) u) t0 a2 ⇒
the thesis becomes
∀H5:nf2 c0 (THead (Bind b) u t0)
.or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind b) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind b) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq T (THead (Bind b) u t0) (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
() by induction hypothesis we know
nf2 c0 u
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T u (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T u (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T u (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i))
() by induction hypothesis we know
nf2 (CHead c0 (Bind b) u) t0
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T t0 (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 (CHead c0 (Bind b) u) w
λw:T.λu0:T.nf2 (CHead (CHead c0 (Bind b) u) (Bind Abst) w) u0
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 (CHead c0 (Bind b) u) ws
λ:TList.λi:nat.nf2 (CHead c0 (Bind b) u) (TLRef i))
suppose H5: nf2 c0 (THead (Bind b) u t0)
suppose : not (eq B Abbr Abst)
suppose : arity g (CHead c0 (Bind Abbr) u) t0 a2
suppose H8: nf2 c0 (THead (Bind Abbr) u t0)
by (nf2_gen_abbr . . . H8 .)
we proved
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abbr) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Abbr) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abbr) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
not (eq B Abbr Abst)
→(arity g (CHead c0 (Bind Abbr) u) t0 a2
→(nf2 c0 (THead (Bind Abbr) u t0)
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abbr) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Abbr) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abbr) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i))))
suppose H6: not (eq B Abst Abst)
suppose : arity g (CHead c0 (Bind Abst) u) t0 a2
suppose : nf2 c0 (THead (Bind Abst) u t0)
(H9)
by (refl_equal . .)
we proved eq B Abst Abst
by (H6 previous)
we proved False
by cases on the previous result we prove
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Abst) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abst) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Abst) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abst) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
end of H9
consider H9
we proved
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Abst) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abst) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
not (eq B Abst Abst)
→(arity g (CHead c0 (Bind Abst) u) t0 a2
→(nf2 c0 (THead (Bind Abst) u t0)
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Abst) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abst) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i))))
suppose : not (eq B Void Abst)
suppose H7: arity g (CHead c0 (Bind Void) u) t0 a2
suppose H8: nf2 c0 (THead (Bind Void) u t0)
(H9)
by (getl_refl . . .)
we proved getl O (CHead c0 (Bind Void) u) (CHead c0 (Bind Void) u)
by (arity_gen_cvoid . . . . H7 . . . previous)
ex T λv:T.eq T t0 (lift (S O) O v)
end of H9
we proceed by induction on H9 to prove
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Void) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Void) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Void) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case ex_intro : x:T H10:eq T t0 (lift (S O) O x) ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Void) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Void) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Void) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
(H11)
we proceed by induction on H10 to prove nf2 c0 (THead (Bind Void) u (lift (S O) O x))
case refl_equal : ⇒
the thesis becomes the hypothesis H8
nf2 c0 (THead (Bind Void) u (lift (S O) O x))
end of H11
by (nf2_gen_void . . . H11 .)
we proved
or3
ex3_2
T
T
λw:T
.λu0:T
.eq
T
THead (Bind Void) u (lift (S O) O x)
THead (Bind Abst) w u0
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex
nat
λn:nat.eq T (THead (Bind Void) u (lift (S O) O x)) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Void) u (lift (S O) O x)
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (eq_ind_r . . . previous . H10)
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Void) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Void) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Void) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
we proved
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Void) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Void) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Void) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
not (eq B Void Abst)
→(arity g (CHead c0 (Bind Void) u) t0 a2
→(nf2 c0 (THead (Bind Void) u t0)
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Void) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Void) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Void) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i))))
by (previous . H0 H3 H5)
we proved
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind b) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind b) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq T (THead (Bind b) u t0) (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
∀H5:nf2 c0 (THead (Bind b) u t0)
.or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind b) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind b) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq T (THead (Bind b) u t0) (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case arity_head : c0:C u:T a1:A :arity g c0 u (asucc g a1) t0:T a2:A :arity g (CHead c0 (Bind Abst) u) t0 a2 ⇒
the thesis becomes
∀H4:nf2 c0 (THead (Bind Abst) u t0)
.or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Abst) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abst) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
() by induction hypothesis we know
nf2 c0 u
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T u (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T u (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T u (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i))
() by induction hypothesis we know
nf2 (CHead c0 (Bind Abst) u) t0
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T t0 (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 (CHead c0 (Bind Abst) u) w
λw:T.λu0:T.nf2 (CHead (CHead c0 (Bind Abst) u) (Bind Abst) w) u0
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 (CHead c0 (Bind Abst) u) ws
λ:TList.λi:nat.nf2 (CHead c0 (Bind Abst) u) (TLRef i))
suppose H4: nf2 c0 (THead (Bind Abst) u t0)
(H5)
by (nf2_gen_abst . . . H4)
land (nf2 c0 u) (nf2 (CHead c0 (Bind Abst) u) t0)
end of H5
we proceed by induction on H5 to prove
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Abst) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abst) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case conj : H6:nf2 c0 u H7:nf2 (CHead c0 (Bind Abst) u) t0 ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Abst) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abst) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (refl_equal . .)
we proved eq T (THead (Bind Abst) u t0) (THead (Bind Abst) u t0)
by (ex3_2_intro . . . . . . . previous H6 H7)
we proved
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
by (or3_intro0 . . . previous)
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Abst) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abst) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
we proved
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Abst) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abst) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
∀H4:nf2 c0 (THead (Bind Abst) u t0)
.or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Bind Abst) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abst) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case arity_appl : c0:C u:T a1:A :arity g c0 u a1 t0:T a2:A H2:arity g c0 t0 (AHead a1 a2) ⇒
the thesis becomes
∀H4:nf2 c0 (THead (Flat Appl) u t0)
.or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
() by induction hypothesis we know
nf2 c0 u
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T u (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T u (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T u (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i))
(H3) by induction hypothesis we know
nf2 c0 t0
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T t0 (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i))
suppose H4: nf2 c0 (THead (Flat Appl) u t0)
(H5)
by (nf2_gen_flat . . . . H4)
land (nf2 c0 u) (nf2 c0 t0)
end of H5
we proceed by induction on H5 to prove
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case conj : H6:nf2 c0 u H7:nf2 c0 t0 ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
(H_x)
by (H3 H7)
or3
ex3_2
T
T
λw:T.λu0:T.eq T t0 (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
end of H_x
(H8) consider H_x
we proceed by induction on H8 to prove
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case or3_intro0 : H9:ex3_2 T T λw:T.λu0:T.eq T t0 (THead (Bind Abst) w u0) λw:T.λ:T.nf2 c0 w λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0 ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
we proceed by induction on H9 to prove
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case ex3_2_intro : x0:T x1:T H10:eq T t0 (THead (Bind Abst) x0 x1) :nf2 c0 x0 :nf2 (CHead c0 (Bind Abst) x0) x1 ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
(H13)
we proceed by induction on H10 to prove nf2 c0 (THead (Flat Appl) u (THead (Bind Abst) x0 x1))
case refl_equal : ⇒
the thesis becomes the hypothesis H4
nf2 c0 (THead (Flat Appl) u (THead (Bind Abst) x0 x1))
end of H13
by (nf2_gen_beta . . . . H13 .)
we proved
or3
ex3_2
T
T
λw:T
.λu0:T
.eq
T
THead (Flat Appl) u (THead (Bind Abst) x0 x1)
THead (Bind Abst) w u0
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex
nat
λn:nat
.eq T (THead (Flat Appl) u (THead (Bind Abst) x0 x1)) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u (THead (Bind Abst) x0 x1)
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (eq_ind_r . . . previous . H10)
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case or3_intro1 : H9:ex nat λn:nat.eq T t0 (TSort n) ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
we proceed by induction on H9 to prove
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case ex_intro : x:nat H10:eq T t0 (TSort x) ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
(H12)
we proceed by induction on H10 to prove arity g c0 (TSort x) (AHead a1 a2)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
arity g c0 (TSort x) (AHead a1 a2)
end of H12
(H_x0)
by (arity_gen_sort . . . . H12)
we proved leq g (AHead a1 a2) (ASort O x)
by (leq_gen_head1 . . . . previous)
ex3_2 A A λa3:A.λ:A.leq g a1 a3 λ:A.λa4:A.leq g a2 a4 λa3:A.λa4:A.eq A (ASort O x) (AHead a3 a4)
end of H_x0
(H13) consider H_x0
we proceed by induction on H13 to prove
or3
ex3_2
T
T
λw:T
.λu0:T
.eq T (THead (Flat Appl) u (TSort x)) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex
nat
λn:nat.eq T (THead (Flat Appl) u (TSort x)) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u (TSort x)
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case ex3_2_intro : x0:A x1:A :leq g a1 x0 :leq g a2 x1 H16:eq A (ASort O x) (AHead x0 x1) ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T
.λu0:T
.eq T (THead (Flat Appl) u (TSort x)) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex
nat
λn:nat.eq T (THead (Flat Appl) u (TSort x)) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u (TSort x)
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
(H17)
we proceed by induction on H16 to prove <λ:A.Prop> CASE AHead x0 x1 OF ASort ⇒True | AHead ⇒False
case refl_equal : ⇒
the thesis becomes <λ:A.Prop> CASE ASort O x OF ASort ⇒True | AHead ⇒False
consider I
we proved True
<λ:A.Prop> CASE ASort O x OF ASort ⇒True | AHead ⇒False
<λ:A.Prop> CASE AHead x0 x1 OF ASort ⇒True | AHead ⇒False
end of H17
consider H17
we proved <λ:A.Prop> CASE AHead x0 x1 OF ASort ⇒True | AHead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or3
ex3_2
T
T
λw:T
.λu0:T
.eq T (THead (Flat Appl) u (TSort x)) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex
nat
λn:nat.eq T (THead (Flat Appl) u (TSort x)) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u (TSort x)
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
or3
ex3_2
T
T
λw:T
.λu0:T
.eq T (THead (Flat Appl) u (TSort x)) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex
nat
λn:nat.eq T (THead (Flat Appl) u (TSort x)) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u (TSort x)
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
we proved
or3
ex3_2
T
T
λw:T
.λu0:T
.eq T (THead (Flat Appl) u (TSort x)) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex
nat
λn:nat.eq T (THead (Flat Appl) u (TSort x)) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u (TSort x)
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (eq_ind_r . . . previous . H10)
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case or3_intro2 : H9:ex3_2 TList nat λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i)) λws:TList.λ:nat.nfs2 c0 ws λ:TList.λi:nat.nf2 c0 (TLRef i) ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
we proceed by induction on H9 to prove
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case ex3_2_intro : x0:TList x1:nat H10:eq T t0 (THeads (Flat Appl) x0 (TLRef x1)) H11:nfs2 c0 x0 H12:nf2 c0 (TLRef x1) ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
(h1)
by (refl_equal . .)
we proved
eq
T
THead (Flat Appl) u (THeads (Flat Appl) x0 (TLRef x1))
THead (Flat Appl) u (THeads (Flat Appl) x0 (TLRef x1))
eq
T
THead (Flat Appl) u (THeads (Flat Appl) x0 (TLRef x1))
THeads (Flat Appl) (TCons u x0) (TLRef x1)
end of h1
(h2)
by (conj . . H6 H11)
we proved land (nf2 c0 u) (nfs2 c0 x0)
nfs2 c0 (TCons u x0)
end of h2
by (ex3_2_intro . . . . . . . h1 h2 H12)
we proved
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u (THeads (Flat Appl) x0 (TLRef x1))
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (or3_intro2 . . . previous)
we proved
or3
ex3_2
T
T
λw:T
.λu0:T
.eq
T
THead (Flat Appl) u (THeads (Flat Appl) x0 (TLRef x1))
THead (Bind Abst) w u0
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex
nat
λn:nat
.eq
T
THead (Flat Appl) u (THeads (Flat Appl) x0 (TLRef x1))
TSort n
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u (THeads (Flat Appl) x0 (TLRef x1))
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (eq_ind_r . . . previous . H10)
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
we proved
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
∀H4:nf2 c0 (THead (Flat Appl) u t0)
.or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Appl) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Appl) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case arity_cast : c0:C u:T a0:A :arity g c0 u (asucc g a0) t0:T :arity g c0 t0 a0 ⇒
the thesis becomes
∀H4:nf2 c0 (THead (Flat Cast) u t0)
.or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Cast) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Cast) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Cast) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
() by induction hypothesis we know
nf2 c0 u
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T u (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T u (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T u (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i))
() by induction hypothesis we know
nf2 c0 t0
→(or3
ex3_2
T
T
λw:T.λu0:T.eq T t0 (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i))
suppose H4: nf2 c0 (THead (Flat Cast) u t0)
by (nf2_gen_cast . . . H4 .)
we proved
or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Cast) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Cast) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Cast) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
∀H4:nf2 c0 (THead (Flat Cast) u t0)
.or3
ex3_2
T
T
λw:T.λu0:T.eq T (THead (Flat Cast) u t0) (THead (Bind Abst) w u0)
λw:T.λ:T.nf2 c0 w
λw:T.λu0:T.nf2 (CHead c0 (Bind Abst) w) u0
ex nat λn:nat.eq T (THead (Flat Cast) u t0) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Flat Cast) u t0
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case arity_repl : c0:C t0:T a1:A :arity g c0 t0 a1 a2:A :leq g a1 a2 ⇒
the thesis becomes
∀H3:nf2 c0 t0
.or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
(H1) by induction hypothesis we know
nf2 c0 t0
→(or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i))
suppose H3: nf2 c0 t0
(H_x)
by (H1 H3)
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case or3_intro0 : H5:ex3_2 T T λw:T.λu:T.eq T t0 (THead (Bind Abst) w u) λw:T.λ:T.nf2 c0 w λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
we proceed by induction on H5 to prove
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case ex3_2_intro : x0:T x1:T H6:eq T t0 (THead (Bind Abst) x0 x1) H7:nf2 c0 x0 H8:nf2 (CHead c0 (Bind Abst) x0) x1 ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (refl_equal . .)
we proved eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) x0 x1)
by (ex3_2_intro . . . . . . . previous H7 H8)
we proved
ex3_2
T
T
λw:T.λu:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
by (or3_intro0 . . . previous)
we proved
or3
ex3_2
T
T
λw:T.λu:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T (THead (Bind Abst) x0 x1) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THead (Bind Abst) x0 x1
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (eq_ind_r . . . previous . H6)
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case or3_intro1 : H5:ex nat λn:nat.eq T t0 (TSort n) ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
we proceed by induction on H5 to prove
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case ex_intro : x:nat H6:eq T t0 (TSort x) ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (refl_equal . .)
we proved eq T (TSort x) (TSort x)
by (ex_intro . . . previous)
we proved ex nat λn:nat.eq T (TSort x) (TSort n)
by (or3_intro1 . . . previous)
we proved
or3
ex3_2
T
T
λw:T.λu:T.eq T (TSort x) (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T (TSort x) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat.eq T (TSort x) (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (eq_ind_r . . . previous . H6)
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case or3_intro2 : H5:ex3_2 TList nat λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i)) λws:TList.λ:nat.nfs2 c0 ws λ:TList.λi:nat.nf2 c0 (TLRef i) ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
we proceed by induction on H5 to prove
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
case ex3_2_intro : x0:TList x1:nat H6:eq T t0 (THeads (Flat Appl) x0 (TLRef x1)) H7:nfs2 c0 x0 H8:nf2 c0 (TLRef x1) ⇒
the thesis becomes
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (refl_equal . .)
we proved
eq
T
THeads (Flat Appl) x0 (TLRef x1)
THeads (Flat Appl) x0 (TLRef x1)
by (ex3_2_intro . . . . . . . previous H7 H8)
we proved
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THeads (Flat Appl) x0 (TLRef x1)
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (or3_intro2 . . . previous)
we proved
or3
ex3_2
T
T
λw:T
.λu:T
.eq T (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T (THeads (Flat Appl) x0 (TLRef x1)) (TSort n)
ex3_2
TList
nat
λws:TList
.λi:nat
.eq
T
THeads (Flat Appl) x0 (TLRef x1)
THeads (Flat Appl) ws (TLRef i)
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
by (eq_ind_r . . . previous . H6)
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
we proved
or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
∀H3:nf2 c0 t0
.or3
ex3_2
T
T
λw:T.λu:T.eq T t0 (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c0 w
λw:T.λu:T.nf2 (CHead c0 (Bind Abst) w) u
ex nat λn:nat.eq T t0 (TSort n)
ex3_2
TList
nat
λws:TList.λi:nat.eq T t0 (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c0 ws
λ:TList.λi:nat.nf2 c0 (TLRef i)
we proved
nf2 c t
→(or3
ex3_2
T
T
λw:T.λu:T.eq T t (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c w
λw:T.λu:T.nf2 (CHead c (Bind Abst) w) u
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))
we proved
∀g:G
.∀c:C
.∀t:T
.∀a:A
.arity g c t a
→(nf2 c t
→(or3
ex3_2
T
T
λw:T.λu:T.eq T t (THead (Bind Abst) w u)
λw:T.λ:T.nf2 c w
λw:T.λu:T.nf2 (CHead c (Bind Abst) w) u
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)))