DEFINITION nf2_dec()
TYPE =
∀c:C.∀t1:T.(or (nf2 c t1) (ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 c t1 t2))
BODY =
assume c: C
(h1)
assume n: nat
assume t1: T
(H_x)
by (nf0_dec .)
or ∀t2:T.(pr0 t1 t2)→(eq T t1 t2) (ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr0 t1 t2)
end of H_x
(H) consider H_x
we proceed by induction on H to prove
or
∀t2:T.(pr2 (CSort n) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CSort n) t1 t2
case or_introl : H0:∀t2:T.(pr0 t1 t2)→(eq T t1 t2) ⇒
the thesis becomes
or
∀t2:T.(pr2 (CSort n) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CSort n) t1 t2
assume t2: T
suppose H1: pr2 (CSort n) t1 t2
(H_y)
by (pr2_gen_csort . . . H1)
pr0 t1 t2
end of H_y
by (H0 . H_y)
we proved eq T t1 t2
we proved ∀t2:T.(pr2 (CSort n) t1 t2)→(eq T t1 t2)
by (or_introl . . previous)
or
∀t2:T.(pr2 (CSort n) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CSort n) t1 t2
case or_intror : H0:ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr0 t1 t2 ⇒
the thesis becomes
or
∀t2:T.(pr2 (CSort n) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CSort n) t1 t2
we proceed by induction on H0 to prove
or
∀t2:T.(pr2 (CSort n) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CSort n) t1 t2
case ex_intro2 : x:T H1:(eq T t1 x)→∀P:Prop.P H2:pr0 t1 x ⇒
the thesis becomes
or
∀t2:T.(pr2 (CSort n) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CSort n) t1 t2
by (pr2_free . . . H2)
we proved pr2 (CSort n) t1 x
by (ex_intro2 . . . . H1 previous)
we proved ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CSort n) t1 t2
by (or_intror . . previous)
or
∀t2:T.(pr2 (CSort n) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CSort n) t1 t2
or
∀t2:T.(pr2 (CSort n) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CSort n) t1 t2
we proved
or
∀t2:T.(pr2 (CSort n) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CSort n) t1 t2
∀n:nat
.∀t1:T
.or
∀t2:T.(pr2 (CSort n) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CSort n) t1 t2
end of h1
(h2)
assume c0: C
suppose H: ∀t1:T.(or ∀t2:T.(pr2 c0 t1 t2)→(eq T t1 t2) (ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 c0 t1 t2))
assume k: K
assume t: T
assume t1: T
(H_x)
by (H .)
or ∀t2:T.(pr2 c0 t1 t2)→(eq T t1 t2) (ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 c0 t1 t2)
end of H_x
(H0) consider H_x
we proceed by induction on H0 to prove
or
∀t2:T.(pr2 (CTail k t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail k t c0) t1 t2
case or_introl : H1:∀t2:T.(pr2 c0 t1 t2)→(eq T t1 t2) ⇒
the thesis becomes
or
∀t2:T.(pr2 (CTail k t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail k t c0) t1 t2
we proceed by induction on k to prove
or
∀t2:T.(pr2 (CTail k t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail k t c0) t1 t2
case Bind : b:B ⇒
the thesis becomes
or
∀t2:T.(pr2 (CTail (Bind b) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind b) t c0) t1 t2
we proceed by induction on b to prove
or
∀t2:T.(pr2 (CTail (Bind b) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind b) t c0) t1 t2
case Abbr : ⇒
the thesis becomes
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
(H_x0)
by (dnf_dec . . .)
ex
T
λv:T
.or
subst0 (clen c0) t t1 (lift (S O) (clen c0) v)
eq T t1 (lift (S O) (clen c0) v)
end of H_x0
(H2) consider H_x0
we proceed by induction on H2 to prove
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
case ex_intro : x:T H3:or (subst0 (clen c0) t t1 (lift (S O) (clen c0) x)) (eq T t1 (lift (S O) (clen c0) x)) ⇒
the thesis becomes
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
we proceed by induction on H3 to prove
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
case or_introl : H4:subst0 (clen c0) t t1 (lift (S O) (clen c0) x) ⇒
the thesis becomes
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
(H_x1)
by (getl_ctail_clen . . .)
ex
nat
λn:nat
.getl
clen c0
CTail (Bind Abbr) t c0
CHead (CSort n) (Bind Abbr) t
end of H_x1
(H5) consider H_x1
we proceed by induction on H5 to prove
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
case ex_intro : x0:nat H6:getl (clen c0) (CTail (Bind Abbr) t c0) (CHead (CSort x0) (Bind Abbr) t) ⇒
the thesis becomes
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
(h1)
suppose H7: eq T t1 (lift (S O) (clen c0) x)
assume P: Prop
(H8)
we proceed by induction on H7 to prove subst0 (clen c0) t (lift (S O) (clen c0) x) (lift (S O) (clen c0) x)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
subst0 (clen c0) t (lift (S O) (clen c0) x) (lift (S O) (clen c0) x)
end of H8
(h1)
by (le_n .)
le (clen c0) (clen c0)
end of h1
(h2)
(h1)
by (le_n .)
we proved le (plus (S O) (clen c0)) (plus (S O) (clen c0))
lt (clen c0) (plus (S O) (clen c0))
end of h1
(h2)
by (plus_sym . .)
eq nat (plus (clen c0) (S O)) (plus (S O) (clen c0))
end of h2
by (eq_ind_r . . . h1 . h2)
lt (clen c0) (plus (clen c0) (S O))
end of h2
by (subst0_gen_lift_false . . . . . . h1 h2 H8 .)
we proved P
(eq T t1 (lift (S O) (clen c0) x))→∀P:Prop.P
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t1 t1
by (pr2_delta . . . . H6 . . previous . H4)
pr2 (CTail (Bind Abbr) t c0) t1 (lift (S O) (clen c0) x)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
by (or_intror . . previous)
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
case or_intror : H4:eq T t1 (lift (S O) (clen c0) x) ⇒
the thesis becomes
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
(H5)
we proceed by induction on H4 to prove
∀t2:T.(pr2 c0 (lift (S O) (clen c0) x) t2)→(eq T (lift (S O) (clen c0) x) t2)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
∀t2:T.(pr2 c0 (lift (S O) (clen c0) x) t2)→(eq T (lift (S O) (clen c0) x) t2)
end of H5
assume t2: T
suppose H6: pr2 (CTail (Bind Abbr) t c0) (lift (S O) (clen c0) x) t2
(H_x1)
by (pr2_gen_ctail . . . . . H6)
or
pr2 c0 (lift (S O) (clen c0) x) t2
ex3
T
λ:T.eq K (Bind Abbr) (Bind Abbr)
λt:T.pr0 (lift (S O) (clen c0) x) t
λt:T.subst0 (clen c0) t t t2
end of H_x1
(H7) consider H_x1
we proceed by induction on H7 to prove eq T (lift (S O) (clen c0) x) t2
case or_introl : H8:pr2 c0 (lift (S O) (clen c0) x) t2 ⇒
the thesis becomes eq T (lift (S O) (clen c0) x) t2
by (H5 . H8)
eq T (lift (S O) (clen c0) x) t2
case or_intror : H8:ex3 T λ:T.eq K (Bind Abbr) (Bind Abbr) λt0:T.pr0 (lift (S O) (clen c0) x) t0 λt0:T.subst0 (clen c0) t t0 t2 ⇒
the thesis becomes eq T (lift (S O) (clen c0) x) t2
we proceed by induction on H8 to prove eq T (lift (S O) (clen c0) x) t2
case ex3_intro : x0:T :eq K (Bind Abbr) (Bind Abbr) H10:pr0 (lift (S O) (clen c0) x) x0 H11:subst0 (clen c0) t x0 t2 ⇒
the thesis becomes eq T (lift (S O) (clen c0) x) t2
by (pr0_gen_lift . . . . H10)
we proved ex2 T λt2:T.eq T x0 (lift (S O) (clen c0) t2) λt2:T.pr0 x t2
we proceed by induction on the previous result to prove eq T (lift (S O) (clen c0) x) t2
case ex_intro2 : x1:T H12:eq T x0 (lift (S O) (clen c0) x1) :pr0 x x1 ⇒
the thesis becomes eq T (lift (S O) (clen c0) x) t2
(H14)
we proceed by induction on H12 to prove subst0 (clen c0) t (lift (S O) (clen c0) x1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H11
subst0 (clen c0) t (lift (S O) (clen c0) x1) t2
end of H14
(h1)
by (le_n .)
le (clen c0) (clen c0)
end of h1
(h2)
(h1)
by (le_n .)
we proved le (plus (S O) (clen c0)) (plus (S O) (clen c0))
lt (clen c0) (plus (S O) (clen c0))
end of h1
(h2)
by (plus_sym . .)
eq nat (plus (clen c0) (S O)) (plus (S O) (clen c0))
end of h2
by (eq_ind_r . . . h1 . h2)
lt (clen c0) (plus (clen c0) (S O))
end of h2
by (subst0_gen_lift_false . . . . . . h1 h2 H14 .)
eq T (lift (S O) (clen c0) x) t2
eq T (lift (S O) (clen c0) x) t2
eq T (lift (S O) (clen c0) x) t2
we proved eq T (lift (S O) (clen c0) x) t2
we proved
∀t2:T
.pr2 (CTail (Bind Abbr) t c0) (lift (S O) (clen c0) x) t2
→eq T (lift (S O) (clen c0) x) t2
by (or_introl . . previous)
we proved
or
∀t2:T
.pr2 (CTail (Bind Abbr) t c0) (lift (S O) (clen c0) x) t2
→eq T (lift (S O) (clen c0) x) t2
ex2
T
λt2:T.(eq T (lift (S O) (clen c0) x) t2)→∀P:Prop.P
λt2:T.pr2 (CTail (Bind Abbr) t c0) (lift (S O) (clen c0) x) t2
by (eq_ind_r . . . previous . H4)
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
or
∀t2:T.(pr2 (CTail (Bind Abbr) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abbr) t c0) t1 t2
case Abst : ⇒
the thesis becomes
or
∀t2:T.(pr2 (CTail (Bind Abst) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abst) t c0) t1 t2
assume t2: T
suppose H2: pr2 (CTail (Bind Abst) t c0) t1 t2
(H_x0)
by (pr2_gen_ctail . . . . . H2)
or
pr2 c0 t1 t2
ex3 T λ:T.eq K (Bind Abst) (Bind Abbr) λt:T.pr0 t1 t λt:T.subst0 (clen c0) t t t2
end of H_x0
(H3) consider H_x0
we proceed by induction on H3 to prove eq T t1 t2
case or_introl : H4:pr2 c0 t1 t2 ⇒
the thesis becomes eq T t1 t2
by (H1 . H4)
eq T t1 t2
case or_intror : H4:ex3 T λ:T.eq K (Bind Abst) (Bind Abbr) λt0:T.pr0 t1 t0 λt0:T.subst0 (clen c0) t t0 t2 ⇒
the thesis becomes eq T t1 t2
we proceed by induction on H4 to prove eq T t1 t2
case ex3_intro : x0:T H5:eq K (Bind Abst) (Bind Abbr) :pr0 t1 x0 :subst0 (clen c0) t x0 t2 ⇒
the thesis becomes eq T t1 t2
(H8)
we proceed by induction on H5 to prove
<λ:K.Prop>
CASE Bind Abbr OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:K.Prop>
CASE Bind Abst OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:K.Prop>
CASE Bind Abst OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
<λ:K.Prop>
CASE Bind Abbr OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
end of H8
consider H8
we proved
<λ:K.Prop>
CASE Bind Abbr OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove eq T t1 t2
eq T t1 t2
eq T t1 t2
we proved eq T t1 t2
we proved ∀t2:T.(pr2 (CTail (Bind Abst) t c0) t1 t2)→(eq T t1 t2)
by (or_introl . . previous)
or
∀t2:T.(pr2 (CTail (Bind Abst) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Abst) t c0) t1 t2
case Void : ⇒
the thesis becomes
or
∀t2:T.(pr2 (CTail (Bind Void) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Void) t c0) t1 t2
assume t2: T
suppose H2: pr2 (CTail (Bind Void) t c0) t1 t2
(H_x0)
by (pr2_gen_ctail . . . . . H2)
or
pr2 c0 t1 t2
ex3 T λ:T.eq K (Bind Void) (Bind Abbr) λt:T.pr0 t1 t λt:T.subst0 (clen c0) t t t2
end of H_x0
(H3) consider H_x0
we proceed by induction on H3 to prove eq T t1 t2
case or_introl : H4:pr2 c0 t1 t2 ⇒
the thesis becomes eq T t1 t2
by (H1 . H4)
eq T t1 t2
case or_intror : H4:ex3 T λ:T.eq K (Bind Void) (Bind Abbr) λt0:T.pr0 t1 t0 λt0:T.subst0 (clen c0) t t0 t2 ⇒
the thesis becomes eq T t1 t2
we proceed by induction on H4 to prove eq T t1 t2
case ex3_intro : x0:T H5:eq K (Bind Void) (Bind Abbr) :pr0 t1 x0 :subst0 (clen c0) t x0 t2 ⇒
the thesis becomes eq T t1 t2
(H8)
we proceed by induction on H5 to prove
<λ:K.Prop>
CASE Bind Abbr OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:K.Prop>
CASE Bind Void OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
consider I
we proved True
<λ:K.Prop>
CASE Bind Void OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
<λ:K.Prop>
CASE Bind Abbr OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
end of H8
consider H8
we proved
<λ:K.Prop>
CASE Bind Abbr OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒False | Void⇒True
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove eq T t1 t2
eq T t1 t2
eq T t1 t2
we proved eq T t1 t2
we proved ∀t2:T.(pr2 (CTail (Bind Void) t c0) t1 t2)→(eq T t1 t2)
by (or_introl . . previous)
or
∀t2:T.(pr2 (CTail (Bind Void) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind Void) t c0) t1 t2
or
∀t2:T.(pr2 (CTail (Bind b) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Bind b) t c0) t1 t2
case Flat : f:F ⇒
the thesis becomes
or
∀t2:T.(pr2 (CTail (Flat f) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Flat f) t c0) t1 t2
assume t2: T
suppose H2: pr2 (CTail (Flat f) t c0) t1 t2
(H_x0)
by (pr2_gen_ctail . . . . . H2)
or
pr2 c0 t1 t2
ex3 T λ:T.eq K (Flat f) (Bind Abbr) λt:T.pr0 t1 t λt:T.subst0 (clen c0) t t t2
end of H_x0
(H3) consider H_x0
we proceed by induction on H3 to prove eq T t1 t2
case or_introl : H4:pr2 c0 t1 t2 ⇒
the thesis becomes eq T t1 t2
by (H1 . H4)
eq T t1 t2
case or_intror : H4:ex3 T λ:T.eq K (Flat f) (Bind Abbr) λt0:T.pr0 t1 t0 λt0:T.subst0 (clen c0) t t0 t2 ⇒
the thesis becomes eq T t1 t2
we proceed by induction on H4 to prove eq T t1 t2
case ex3_intro : x0:T H5:eq K (Flat f) (Bind Abbr) :pr0 t1 x0 :subst0 (clen c0) t x0 t2 ⇒
the thesis becomes eq T t1 t2
(H8)
we proceed by induction on H5 to prove <λ:K.Prop> CASE Bind Abbr OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes <λ:K.Prop> CASE Flat f OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:K.Prop> CASE Flat f OF Bind ⇒False | Flat ⇒True
<λ:K.Prop> CASE Bind Abbr OF Bind ⇒False | Flat ⇒True
end of H8
consider H8
we proved <λ:K.Prop> CASE Bind Abbr OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove eq T t1 t2
eq T t1 t2
eq T t1 t2
we proved eq T t1 t2
we proved ∀t2:T.(pr2 (CTail (Flat f) t c0) t1 t2)→(eq T t1 t2)
by (or_introl . . previous)
or
∀t2:T.(pr2 (CTail (Flat f) t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail (Flat f) t c0) t1 t2
or
∀t2:T.(pr2 (CTail k t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail k t c0) t1 t2
case or_intror : H1:ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 c0 t1 t2 ⇒
the thesis becomes
or
∀t2:T.(pr2 (CTail k t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail k t c0) t1 t2
we proceed by induction on H1 to prove
or
∀t2:T.(pr2 (CTail k t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail k t c0) t1 t2
case ex_intro2 : x:T H2:(eq T t1 x)→∀P:Prop.P H3:pr2 c0 t1 x ⇒
the thesis becomes
or
∀t2:T.(pr2 (CTail k t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail k t c0) t1 t2
by (pr2_ctail . . . H3 . .)
we proved pr2 (CTail k t c0) t1 x
by (ex_intro2 . . . . H2 previous)
we proved ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail k t c0) t1 t2
by (or_intror . . previous)
or
∀t2:T.(pr2 (CTail k t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail k t c0) t1 t2
or
∀t2:T.(pr2 (CTail k t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail k t c0) t1 t2
we proved
or
∀t2:T.(pr2 (CTail k t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail k t c0) t1 t2
∀c0:C
.∀t1:T.(or ∀t2:T.(pr2 c0 t1 t2)→(eq T t1 t2) (ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 c0 t1 t2))
→∀k:K
.∀t:T
.∀t1:T
.or
∀t2:T.(pr2 (CTail k t c0) t1 t2)→(eq T t1 t2)
ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 (CTail k t c0) t1 t2
end of h2
by (c_tail_ind . h1 h2 .)
we proved ∀t1:T.(or ∀t2:T.(pr2 c t1 t2)→(eq T t1 t2) (ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 c t1 t2))
that is equivalent to ∀t1:T.(or (nf2 c t1) (ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 c t1 t2))
we proved ∀c:C.∀t1:T.(or (nf2 c t1) (ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 c t1 t2))