DEFINITION ty3_nf2_inv_sort()
TYPE =
∀g:G
.∀c:C
.∀t:T
.∀m:nat
.ty3 g c t (TSort m)
→(nf2 c t
→(or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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 m: nat
suppose H: ty3 g c t (TSort m)
suppose H0: nf2 c t
(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
(H1) consider H_x
we proceed by induction on H1 to prove
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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 or3_intro0 : H2: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 ⇒
the thesis becomes
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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 proceed by induction on H2 to prove
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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 ex3_2_intro : x0:T x1:T H3:eq T t (THead (Bind Abst) x0 x1) :nf2 c x0 :nf2 (CHead c (Bind Abst) x0) x1 ⇒
the thesis becomes
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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)
(H6)
we proceed by induction on H3 to prove ty3 g c (THead (Bind Abst) x0 x1) (TSort m)
case refl_equal : ⇒
the thesis becomes the hypothesis H
ty3 g c (THead (Bind Abst) x0 x1) (TSort m)
end of H6
by (ty3_gen_bind . . . . . . H6)
we proved
ex3_2
T
T
λt2:T.λ:T.pc3 c (THead (Bind Abst) x0 t2) (TSort m)
λ: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
or
ex2
nat
λn:nat.eq T (THead (Bind Abst) x0 x1) (TSort n)
λn:nat.eq nat m (next g 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 c ws
λ:TList.λi:nat.nf2 c (TLRef i)
case ex3_2_intro : x2:T x3:T H7:pc3 c (THead (Bind Abst) x0 x2) (TSort m) :ty3 g c x0 x3 :ty3 g (CHead c (Bind Abst) x0) x1 x2 ⇒
the thesis becomes
or
ex2
nat
λn:nat.eq T (THead (Bind Abst) x0 x1) (TSort n)
λn:nat.eq nat m (next g 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 c ws
λ:TList.λi:nat.nf2 c (TLRef i)
by (pc3_s . . . H7)
we proved pc3 c (TSort m) (THead (Bind Abst) x0 x2)
by (pc3_gen_sort_abst . . . . previous .)
or
ex2
nat
λn:nat.eq T (THead (Bind Abst) x0 x1) (TSort n)
λn:nat.eq nat m (next g 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 c ws
λ:TList.λi:nat.nf2 c (TLRef i)
we proved
or
ex2
nat
λn:nat.eq T (THead (Bind Abst) x0 x1) (TSort n)
λn:nat.eq nat m (next g 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 c ws
λ:TList.λi:nat.nf2 c (TLRef i)
by (eq_ind_r . . . previous . H3)
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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)
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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 or3_intro1 : H2:ex nat λn:nat.eq T t (TSort n) ⇒
the thesis becomes
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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 proceed by induction on H2 to prove
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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 ex_intro : x:nat H3:eq T t (TSort x) ⇒
the thesis becomes
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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)
(H4)
we proceed by induction on H3 to prove ty3 g c (TSort x) (TSort m)
case refl_equal : ⇒
the thesis becomes the hypothesis H
ty3 g c (TSort x) (TSort m)
end of H4
by (ty3_gen_sort . . . . H4)
we proved pc3 c (TSort (next g x)) (TSort m)
by (pc3_gen_sort . . . previous)
we proved eq nat (next g x) m
we proceed by induction on the previous result to prove
or
ex2 nat λn0:nat.eq T (TSort x) (TSort n0) λn0:nat.eq nat m (next g n0)
ex3_2
TList
nat
λws:TList
.λi:nat.eq T (TSort x) (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c ws
λ:TList.λi:nat.nf2 c (TLRef i)
case refl_equal : ⇒
the thesis becomes
or
ex2
nat
λn:nat.eq T (TSort x) (TSort n)
λn:nat.eq nat (next g x) (next g n)
ex3_2
TList
nat
λws:TList
.λi:nat.eq T (TSort x) (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c ws
λ:TList.λi:nat.nf2 c (TLRef i)
(h1)
by (refl_equal . .)
eq T (TSort x) (TSort x)
end of h1
(h2)
by (refl_equal . .)
eq nat (next g x) (next g x)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
nat
λn:nat.eq T (TSort x) (TSort n)
λn:nat.eq nat (next g x) (next g n)
by (or_introl . . previous)
or
ex2
nat
λn:nat.eq T (TSort x) (TSort n)
λn:nat.eq nat (next g x) (next g n)
ex3_2
TList
nat
λws:TList
.λi:nat.eq T (TSort x) (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c ws
λ:TList.λi:nat.nf2 c (TLRef i)
we proved
or
ex2 nat λn0:nat.eq T (TSort x) (TSort n0) λn0:nat.eq nat m (next g n0)
ex3_2
TList
nat
λws:TList
.λi:nat.eq T (TSort x) (THeads (Flat Appl) ws (TLRef i))
λws:TList.λ:nat.nfs2 c ws
λ:TList.λi:nat.nf2 c (TLRef i)
by (eq_ind_r . . . previous . H3)
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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)
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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 or3_intro2 : H2: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
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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 proceed by induction on H2 to prove
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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 ex3_2_intro : x0:TList x1:nat H3:eq T t (THeads (Flat Appl) x0 (TLRef x1)) H4:nfs2 c x0 H5:nf2 c (TLRef x1) ⇒
the thesis becomes
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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)
by (refl_equal . .)
we proved
eq
T
THeads (Flat Appl) x0 (TLRef x1)
THeads (Flat Appl) x0 (TLRef x1)
by (ex3_2_intro . . . . . . . previous H4 H5)
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 c ws
λ:TList.λi:nat.nf2 c (TLRef i)
by (or_intror . . previous)
we proved
or
ex2
nat
λn:nat.eq T (THeads (Flat Appl) x0 (TLRef x1)) (TSort n)
λn:nat.eq nat m (next g 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 c ws
λ:TList.λi:nat.nf2 c (TLRef i)
by (eq_ind_r . . . previous . H3)
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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)
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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
or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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
.∀m:nat
.ty3 g c t (TSort m)
→(nf2 c t
→(or
ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g 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)))