DEFINITION ex2_nf2()
TYPE =
nf2 ex2_c ex2_t
BODY =
we must prove nf2 ex2_c ex2_t
or equivalently ∀t2:T.(pr2 ex2_c ex2_t t2)→(eq T ex2_t t2)
assume t2: T
we must prove (pr2 ex2_c ex2_t t2)→(eq T ex2_t t2)
or equivalently
pr2 (CSort O) (THead (Flat Appl) (TSort O) (TSort O)) t2
→eq T ex2_t t2
suppose H: pr2 (CSort O) (THead (Flat Appl) (TSort O) (TSort O)) t2
(H0)
by (pr2_gen_appl . . . . H)
or3
ex3_2
T
T
λu2:T.λt2:T.eq T t2 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr2 (CSort O) (TSort O) u2
λ:T.λt2:T.pr2 (CSort O) (TSort O) t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T (TSort O) (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T t2 (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr2 (CSort O) (TSort O) u2
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead (CSort O) (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T (TSort O) (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T
.λy2:T.eq T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr2 (CSort O) (TSort O) u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr2 (CSort O) y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr2 (CHead (CSort O) (Bind b) y2) z1 z2
end of H0
we proceed by induction on H0 to prove eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
case or3_intro0 : H1:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr2 (CSort O) (TSort O) u2 λ:T.λt3:T.pr2 (CSort O) (TSort O) t3 ⇒
the thesis becomes eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
we proceed by induction on H1 to prove eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
case ex3_2_intro : x0:T x1:T H2:eq T t2 (THead (Flat Appl) x0 x1) H3:pr2 (CSort O) (TSort O) x0 H4:pr2 (CSort O) (TSort O) x1 ⇒
the thesis becomes eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
(H5)
by (pr2_gen_sort . . . H4)
we proved eq T x1 (TSort O)
we proceed by induction on the previous result to prove eq T t2 (THead (Flat Appl) x0 (TSort O))
case refl_equal : ⇒
the thesis becomes the hypothesis H2
eq T t2 (THead (Flat Appl) x0 (TSort O))
end of H5
(H6)
by (pr2_gen_sort . . . H3)
we proved eq T x0 (TSort O)
we proceed by induction on the previous result to prove eq T t2 (THead (Flat Appl) (TSort O) (TSort O))
case refl_equal : ⇒
the thesis becomes the hypothesis H5
eq T t2 (THead (Flat Appl) (TSort O) (TSort O))
end of H6
by (refl_equal . .)
we proved
eq
T
THead (Flat Appl) (TSort O) (TSort O)
THead (Flat Appl) (TSort O) (TSort O)
by (eq_ind_r . . . previous . H6)
eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
case or3_intro1 : H1:ex4_4 T T T T λy1:T.λz1:T.λ:T.λ:T.eq T (TSort O) (THead (Bind Abst) y1 z1) λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3) λ:T.λ:T.λu2:T.λ:T.pr2 (CSort O) (TSort O) u2 λ:T.λz1:T.λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead (CSort O) (Bind b) u) z1 t3) ⇒
the thesis becomes eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
we proceed by induction on H1 to prove eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
case ex4_4_intro : x0:T x1:T x2:T x3:T H2:eq T (TSort O) (THead (Bind Abst) x0 x1) H3:eq T t2 (THead (Bind Abbr) x2 x3) H4:pr2 (CSort O) (TSort O) x2 :∀b:B.∀u:T.(pr2 (CHead (CSort O) (Bind b) u) x1 x3) ⇒
the thesis becomes eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
(H6)
by (pr2_gen_sort . . . H4)
we proved eq T x2 (TSort O)
we proceed by induction on the previous result to prove eq T t2 (THead (Bind Abbr) (TSort O) x3)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq T t2 (THead (Bind Abbr) (TSort O) x3)
end of H6
(H7)
we proceed by induction on H2 to prove
<λ:T.Prop>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort O OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort O OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H7
consider H7
we proved
<λ:T.Prop>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
eq
T
THead (Flat Appl) (TSort O) (TSort O)
THead (Bind Abbr) (TSort O) x3
we proved
eq
T
THead (Flat Appl) (TSort O) (TSort O)
THead (Bind Abbr) (TSort O) x3
by (eq_ind_r . . . previous . H6)
eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
case or3_intro2 : H1:ex6_6 B T T T T T λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst) λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T (TSort O) (THead (Bind b) y1 z1) λb:B.λ:T.λ:T.λz2:T.λu2:T.λy2:T.eq T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr2 (CSort O) (TSort O) u2 λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr2 (CSort O) y1 y2 λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr2 (CHead (CSort O) (Bind b) y2) z1 z2 ⇒
the thesis becomes eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
we proceed by induction on H1 to prove eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
case ex6_6_intro : x0:B x1:T x2:T x3:T x4:T x5:T :not (eq B x0 Abst) H3:eq T (TSort O) (THead (Bind x0) x1 x2) H4:eq T t2 (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)) H5:pr2 (CSort O) (TSort O) x4 H6:pr2 (CSort O) x1 x5 :pr2 (CHead (CSort O) (Bind x0) x5) x2 x3 ⇒
the thesis becomes eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
(H8)
by (pr2_gen_sort . . . H5)
we proved eq T x4 (TSort O)
we proceed by induction on the previous result to prove
eq
T
t2
THead
Bind x0
x5
THead (Flat Appl) (lift (S O) O (TSort O)) x3
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq
T
t2
THead
Bind x0
x5
THead (Flat Appl) (lift (S O) O (TSort O)) x3
end of H8
(H9)
we proceed by induction on H3 to prove
<λ:T.Prop>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort O OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort O OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H9
consider H9
we proved
<λ:T.Prop>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
eq
T
THead (Flat Appl) (TSort O) (TSort O)
THead
Bind x0
x5
THead (Flat Appl) (lift (S O) O (TSort O)) x3
we proved
eq
T
THead (Flat Appl) (TSort O) (TSort O)
THead
Bind x0
x5
THead (Flat Appl) (lift (S O) O (TSort O)) x3
by (eq_ind_r . . . previous . H8)
eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
we proved eq T (THead (Flat Appl) (TSort O) (TSort O)) t2
that is equivalent to eq T ex2_t t2
we proved
pr2 (CSort O) (THead (Flat Appl) (TSort O) (TSort O)) t2
→eq T ex2_t t2
that is equivalent to (pr2 ex2_c ex2_t t2)→(eq T ex2_t t2)
we proved ∀t2:T.(pr2 ex2_c ex2_t t2)→(eq T ex2_t t2)
that is equivalent to nf2 ex2_c ex2_t