DEFINITION nf0_dec()
TYPE =
∀t1:T.(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))
BODY =
assume t1: T
we proceed by induction on t1 to prove 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)
case TSort : n:nat ⇒
the thesis becomes
or
∀t2:T.(pr0 (TSort n) t2)→(eq T (TSort n) t2)
ex2 T λt2:T.(eq T (TSort n) t2)→∀P:Prop.P λt2:T.pr0 (TSort n) t2
assume t2: T
suppose H: pr0 (TSort n) t2
(h1)
by (refl_equal . .)
eq T (TSort n) (TSort n)
end of h1
(h2)
by (pr0_gen_sort . . H)
eq T t2 (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq T (TSort n) t2
we proved ∀t2:T.(pr0 (TSort n) t2)→(eq T (TSort n) t2)
by (or_introl . . previous)
or
∀t2:T.(pr0 (TSort n) t2)→(eq T (TSort n) t2)
ex2 T λt2:T.(eq T (TSort n) t2)→∀P:Prop.P λt2:T.pr0 (TSort n) t2
case TLRef : n:nat ⇒
the thesis becomes
or
∀t2:T.(pr0 (TLRef n) t2)→(eq T (TLRef n) t2)
ex2 T λt2:T.(eq T (TLRef n) t2)→∀P:Prop.P λt2:T.pr0 (TLRef n) t2
assume t2: T
suppose H: pr0 (TLRef n) t2
(h1)
by (refl_equal . .)
eq T (TLRef n) (TLRef n)
end of h1
(h2)
by (pr0_gen_lref . . H)
eq T t2 (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq T (TLRef n) t2
we proved ∀t2:T.(pr0 (TLRef n) t2)→(eq T (TLRef n) t2)
by (or_introl . . previous)
or
∀t2:T.(pr0 (TLRef n) t2)→(eq T (TLRef n) t2)
ex2 T λt2:T.(eq T (TLRef n) t2)→∀P:Prop.P λt2:T.pr0 (TLRef n) t2
case THead : k:K t:T t0:T ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead k t t0) t2)→(eq T (THead k t t0) t2)
ex2 T λt2:T.(eq T (THead k t t0) t2)→∀P:Prop.P λt2:T.pr0 (THead k t t0) t2
(H) by induction hypothesis we know or ∀t2:T.(pr0 t t2)→(eq T t t2) (ex2 T λt2:T.(eq T t t2)→∀P:Prop.P λt2:T.pr0 t t2)
(H0) by induction hypothesis we know or ∀t2:T.(pr0 t0 t2)→(eq T t0 t2) (ex2 T λt2:T.(eq T t0 t2)→∀P:Prop.P λt2:T.pr0 t0 t2)
we proceed by induction on k to prove
or
∀t2:T.(pr0 (THead k t t0) t2)→(eq T (THead k t t0) t2)
ex2 T λt2:T.(eq T (THead k t t0) t2)→∀P:Prop.P λt2:T.pr0 (THead k t t0) t2
case Bind : b:B ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind b) t t0) t2)→(eq T (THead (Bind b) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind b) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind b) t t0) t2
we proceed by induction on b to prove
or
∀t2:T.(pr0 (THead (Bind b) t t0) t2)→(eq T (THead (Bind b) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind b) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind b) t t0) t2
case Abbr : ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Abbr) t t0) t2)→(eq T (THead (Bind Abbr) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abbr) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abbr) t t0) t2
(H_x)
by (dnf_dec . . .)
ex T λv:T.or (subst0 O t t0 (lift (S O) O v)) (eq T t0 (lift (S O) O v))
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove
ex2
T
λt2:T.(eq T (THead (Bind Abbr) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abbr) t t0) t2
case ex_intro : x:T H2:or (subst0 O t t0 (lift (S O) O x)) (eq T t0 (lift (S O) O x)) ⇒
the thesis becomes
ex2
T
λt2:T.(eq T (THead (Bind Abbr) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abbr) t t0) t2
we proceed by induction on H2 to prove
ex2
T
λt2:T.(eq T (THead (Bind Abbr) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abbr) t t0) t2
case or_introl : H3:subst0 O t t0 (lift (S O) O x) ⇒
the thesis becomes
ex2
T
λt2:T.(eq T (THead (Bind Abbr) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abbr) t t0) t2
(h1)
suppose H4:
eq
T
THead (Bind Abbr) t t0
THead (Bind Abbr) t (lift (S O) O x)
assume P: Prop
(H5)
by (f_equal . . . . . H4)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) t t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
<λ:T.T>
CASE THead (Bind Abbr) t (lift (S O) O x) OF
TSort ⇒t0
| TLRef ⇒t0
| THead t2⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
THead (Bind Abbr) t t0
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
THead (Bind Abbr) t (lift (S O) O x)
end of H5
(H6)
consider H5
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) t t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
<λ:T.T>
CASE THead (Bind Abbr) t (lift (S O) O x) OF
TSort ⇒t0
| TLRef ⇒t0
| THead t2⇒t2
that is equivalent to eq T t0 (lift (S O) O x)
we proceed by induction on the previous result to prove subst0 O t (lift (S O) O x) (lift (S O) O x)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 O t (lift (S O) O x) (lift (S O) O x)
end of H6
by (subst0_refl . . . H6 .)
we proved P
(eq
T
THead (Bind Abbr) t t0
THead (Bind Abbr) t (lift (S O) O x))
→∀P:Prop.P
end of h1
(h2)
(h1) by (pr0_refl .) we proved pr0 t t
(h2) by (pr0_refl .) we proved pr0 t0 t0
by (pr0_delta . . h1 . . h2 . H3)
pr0
THead (Bind Abbr) t t0
THead (Bind Abbr) t (lift (S O) O x)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
T
λt2:T.(eq T (THead (Bind Abbr) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abbr) t t0) t2
case or_intror : H3:eq T t0 (lift (S O) O x) ⇒
the thesis becomes
ex2
T
λt3:T.(eq T (THead (Bind Abbr) t t0) t3)→∀P:Prop.P
λt3:T.pr0 (THead (Bind Abbr) t t0) t3
(h1)
suppose H4: eq T (THead (Bind Abbr) t (lift (S O) O x)) x
assume P: Prop
by (thead_x_lift_y_y . . . . . H4 .)
we proved P
(eq T (THead (Bind Abbr) t (lift (S O) O x)) x)→∀P:Prop.P
end of h1
(h2)
by (pr0_refl .)
we proved pr0 x x
by (pr0_zeta . not_abbr_abst . . previous .)
pr0 (THead (Bind Abbr) t (lift (S O) O x)) x
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T.(eq T (THead (Bind Abbr) t (lift (S O) O x)) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abbr) t (lift (S O) O x)) t2
by (eq_ind_r . . . previous . H3)
ex2
T
λt3:T.(eq T (THead (Bind Abbr) t t0) t3)→∀P:Prop.P
λt3:T.pr0 (THead (Bind Abbr) t t0) t3
ex2
T
λt2:T.(eq T (THead (Bind Abbr) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abbr) t t0) t2
we proved
ex2
T
λt2:T.(eq T (THead (Bind Abbr) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abbr) t t0) t2
by (or_intror . . previous)
or
∀t2:T.(pr0 (THead (Bind Abbr) t t0) t2)→(eq T (THead (Bind Abbr) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abbr) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abbr) t t0) t2
case Abst : ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
(H1) consider H
we proceed by induction on H1 to prove
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
case or_introl : H2:∀t2:T.(pr0 t t2)→(eq T t t2) ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
(H3) consider H0
we proceed by induction on H3 to prove
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
case or_introl : H4:∀t2:T.(pr0 t0 t2)→(eq T t0 t2) ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
assume t2: T
suppose H5: pr0 (THead (Bind Abst) t t0) t2
by (pr0_gen_abst . . . H5)
we proved ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Bind Abst) u2 t2) λu2:T.λ:T.pr0 t u2 λ:T.λt2:T.pr0 t0 t2
we proceed by induction on the previous result to prove eq T (THead (Bind Abst) t t0) t2
case ex3_2_intro : x0:T x1:T H6:eq T t2 (THead (Bind Abst) x0 x1) H7:pr0 t x0 H8:pr0 t0 x1 ⇒
the thesis becomes eq T (THead (Bind Abst) t t0) t2
(H_y) by (H4 . H8) we proved eq T t0 x1
(H_y0) by (H2 . H7) we proved eq T t x0
(H10)
by (eq_ind_r . . . H6 . H_y)
eq T t2 (THead (Bind Abst) x0 t0)
end of H10
(H12)
by (eq_ind_r . . . H10 . H_y0)
eq T t2 (THead (Bind Abst) t t0)
end of H12
by (refl_equal . .)
we proved eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t t0)
by (eq_ind_r . . . previous . H12)
eq T (THead (Bind Abst) t t0) t2
we proved eq T (THead (Bind Abst) t t0) t2
we proved
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
by (or_introl . . previous)
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
case or_intror : H4:ex2 T λt2:T.(eq T t0 t2)→∀P:Prop.P λt2:T.pr0 t0 t2 ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
we proceed by induction on H4 to prove
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
case ex_intro2 : x:T H5:(eq T t0 x)→∀P:Prop.P H6:pr0 t0 x ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
(h1)
suppose H7: eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t x)
assume P: Prop
(H8)
by (f_equal . . . . . H7)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
<λ:T.T> CASE THead (Bind Abst) t x OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
THead (Bind Abst) t t0
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
THead (Bind Abst) t x
end of H8
(H10)
consider H8
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
<λ:T.T> CASE THead (Bind Abst) t x OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
that is equivalent to eq T t0 x
by (eq_ind_r . . . H5 . previous)
(eq T t0 t0)→∀P0:Prop.P0
end of H10
by (refl_equal . .)
we proved eq T t0 t0
by (H10 previous .)
we proved P
eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t x)
→∀P:Prop.P
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t t
by (pr0_comp . . previous . . H6 .)
pr0 (THead (Bind Abst) t t0) (THead (Bind Abst) t x)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
by (or_intror . . previous)
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
case or_intror : H2:ex2 T λt2:T.(eq T t t2)→∀P:Prop.P λt2:T.pr0 t t2 ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
we proceed by induction on H2 to prove
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
case ex_intro2 : x:T H3:(eq T t x)→∀P:Prop.P H4:pr0 t x ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
(h1)
suppose H5: eq T (THead (Bind Abst) t t0) (THead (Bind Abst) x t0)
assume P: Prop
(H6)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
<λ:T.T> CASE THead (Bind Abst) x t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
THead (Bind Abst) t t0
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
THead (Bind Abst) x t0
end of H6
(H8)
consider H6
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
<λ:T.T> CASE THead (Bind Abst) x t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
that is equivalent to eq T t x
by (eq_ind_r . . . H3 . previous)
(eq T t t)→∀P0:Prop.P0
end of H8
by (refl_equal . .)
we proved eq T t t
by (H8 previous .)
we proved P
eq T (THead (Bind Abst) t t0) (THead (Bind Abst) x t0)
→∀P:Prop.P
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t0 t0
by (pr0_comp . . H4 . . previous .)
pr0 (THead (Bind Abst) t t0) (THead (Bind Abst) x t0)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
by (or_intror . . previous)
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
or
∀t2:T.(pr0 (THead (Bind Abst) t t0) t2)→(eq T (THead (Bind Abst) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) t t0) t2
case Void : ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
(H_x)
by (dnf_dec . . .)
ex T λv:T.or (subst0 O t t0 (lift (S O) O v)) (eq T t0 (lift (S O) O v))
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
case ex_intro : x:T H2:or (subst0 O t t0 (lift (S O) O x)) (eq T t0 (lift (S O) O x)) ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
we proceed by induction on H2 to prove
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
case or_introl : H3:subst0 O t t0 (lift (S O) O x) ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
(H4) consider H
we proceed by induction on H4 to prove
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
case or_introl : H5:∀t2:T.(pr0 t t2)→(eq T t t2) ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
(H6) consider H0
we proceed by induction on H6 to prove
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
case or_introl : H7:∀t2:T.(pr0 t0 t2)→(eq T t0 t2) ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
assume t2: T
suppose H8: pr0 (THead (Bind Void) t t0) t2
by (pr0_gen_void . . . H8)
we proved
or
ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Bind Void) u2 t2) λu2:T.λ:T.pr0 t u2 λ:T.λt2:T.pr0 t0 t2
pr0 t0 (lift (S O) O t2)
we proceed by induction on the previous result to prove eq T (THead (Bind Void) t t0) t2
case or_introl : H9:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Bind Void) u2 t3) λu2:T.λ:T.pr0 t u2 λ:T.λt3:T.pr0 t0 t3 ⇒
the thesis becomes eq T (THead (Bind Void) t t0) t2
we proceed by induction on H9 to prove eq T (THead (Bind Void) t t0) t2
case ex3_2_intro : x0:T x1:T H10:eq T t2 (THead (Bind Void) x0 x1) H11:pr0 t x0 H12:pr0 t0 x1 ⇒
the thesis becomes eq T (THead (Bind Void) t t0) t2
(H_y) by (H7 . H12) we proved eq T t0 x1
(H_y0) by (H5 . H11) we proved eq T t x0
(H14)
by (eq_ind_r . . . H10 . H_y)
eq T t2 (THead (Bind Void) x0 t0)
end of H14
(H16)
by (eq_ind_r . . . H14 . H_y0)
eq T t2 (THead (Bind Void) t t0)
end of H16
by (refl_equal . .)
we proved eq T (THead (Bind Void) t t0) (THead (Bind Void) t t0)
by (eq_ind_r . . . previous . H16)
eq T (THead (Bind Void) t t0) t2
eq T (THead (Bind Void) t t0) t2
case or_intror : H9:pr0 t0 (lift (S O) O t2) ⇒
the thesis becomes eq T (THead (Bind Void) t t0) t2
(H_y)
by (H7 . H9)
eq T t0 (lift (S O) O t2)
end of H_y
(H10)
we proceed by induction on H_y to prove subst0 O t (lift (S O) O t2) (lift (S O) O x)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 O t (lift (S O) O t2) (lift (S O) O x)
end of H10
(h1) by (le_n .) we proved le O O
(h2)
(h1)
by (le_n .)
we proved le (plus (S O) O) (plus (S O) O)
lt O (plus (S O) O)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus O (S O)) (plus (S O) O)
end of h2
by (eq_ind_r . . . h1 . h2)
lt O (plus O (S O))
end of h2
by (subst0_gen_lift_false . . . . . . h1 h2 H10 .)
we proved eq T (THead (Bind Void) t (lift (S O) O t2)) t2
by (eq_ind_r . . . previous . H_y)
eq T (THead (Bind Void) t t0) t2
we proved eq T (THead (Bind Void) t t0) t2
we proved
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
by (or_introl . . previous)
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
case or_intror : H7:ex2 T λt2:T.(eq T t0 t2)→∀P:Prop.P λt2:T.pr0 t0 t2 ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
we proceed by induction on H7 to prove
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
case ex_intro2 : x0:T H8:(eq T t0 x0)→∀P:Prop.P H9:pr0 t0 x0 ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
(h1)
suppose H10: eq T (THead (Bind Void) t t0) (THead (Bind Void) t x0)
assume P: Prop
(H11)
by (f_equal . . . . . H10)
we proved
eq
T
<λ:T.T> CASE THead (Bind Void) t t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
<λ:T.T> CASE THead (Bind Void) t x0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
THead (Bind Void) t t0
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
THead (Bind Void) t x0
end of H11
(H13)
consider H11
we proved
eq
T
<λ:T.T> CASE THead (Bind Void) t t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
<λ:T.T> CASE THead (Bind Void) t x0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
that is equivalent to eq T t0 x0
by (eq_ind_r . . . H8 . previous)
(eq T t0 t0)→∀P0:Prop.P0
end of H13
by (refl_equal . .)
we proved eq T t0 t0
by (H13 previous .)
we proved P
eq T (THead (Bind Void) t t0) (THead (Bind Void) t x0)
→∀P:Prop.P
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t t
by (pr0_comp . . previous . . H9 .)
pr0 (THead (Bind Void) t t0) (THead (Bind Void) t x0)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
by (or_intror . . previous)
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
case or_intror : H5:ex2 T λt2:T.(eq T t t2)→∀P:Prop.P λt2:T.pr0 t t2 ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
we proceed by induction on H5 to prove
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
case ex_intro2 : x0:T H6:(eq T t x0)→∀P:Prop.P H7:pr0 t x0 ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
(h1)
suppose H8: eq T (THead (Bind Void) t t0) (THead (Bind Void) x0 t0)
assume P: Prop
(H9)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead (Bind Void) t t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
<λ:T.T> CASE THead (Bind Void) x0 t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
THead (Bind Void) t t0
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
THead (Bind Void) x0 t0
end of H9
(H11)
consider H9
we proved
eq
T
<λ:T.T> CASE THead (Bind Void) t t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
<λ:T.T> CASE THead (Bind Void) x0 t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
that is equivalent to eq T t x0
by (eq_ind_r . . . H6 . previous)
(eq T t t)→∀P0:Prop.P0
end of H11
by (refl_equal . .)
we proved eq T t t
by (H11 previous .)
we proved P
eq T (THead (Bind Void) t t0) (THead (Bind Void) x0 t0)
→∀P:Prop.P
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t0 t0
by (pr0_comp . . H7 . . previous .)
pr0 (THead (Bind Void) t t0) (THead (Bind Void) x0 t0)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
by (or_intror . . previous)
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
case or_intror : H3:eq T t0 (lift (S O) O x) ⇒
the thesis becomes
or
∀t3:T.(pr0 (THead (Bind Void) t t0) t3)→(eq T (THead (Bind Void) t t0) t3)
ex2
T
λt3:T.(eq T (THead (Bind Void) t t0) t3)→∀P:Prop.P
λt3:T.pr0 (THead (Bind Void) t t0) t3
(h1)
suppose H5: eq T (THead (Bind Void) t (lift (S O) O x)) x
assume P: Prop
by (thead_x_lift_y_y . . . . . H5 .)
we proved P
(eq T (THead (Bind Void) t (lift (S O) O x)) x)→∀P:Prop.P
end of h1
(h2)
(h1)
by (sym_not_eq . . . not_abst_void)
not (eq B Void Abst)
end of h1
(h2) by (pr0_refl .) we proved pr0 x x
by (pr0_zeta . h1 . . h2 .)
pr0 (THead (Bind Void) t (lift (S O) O x)) x
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T.(eq T (THead (Bind Void) t (lift (S O) O x)) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t (lift (S O) O x)) t2
by (or_intror . . previous)
we proved
or
∀t2:T
.pr0 (THead (Bind Void) t (lift (S O) O x)) t2
→eq T (THead (Bind Void) t (lift (S O) O x)) t2
ex2
T
λt2:T.(eq T (THead (Bind Void) t (lift (S O) O x)) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t (lift (S O) O x)) t2
by (eq_ind_r . . . previous . H3)
or
∀t3:T.(pr0 (THead (Bind Void) t t0) t3)→(eq T (THead (Bind Void) t t0) t3)
ex2
T
λt3:T.(eq T (THead (Bind Void) t t0) t3)→∀P:Prop.P
λt3:T.pr0 (THead (Bind Void) t t0) t3
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
or
∀t2:T.(pr0 (THead (Bind Void) t t0) t2)→(eq T (THead (Bind Void) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) t t0) t2
or
∀t2:T.(pr0 (THead (Bind b) t t0) t2)→(eq T (THead (Bind b) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Bind b) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind b) t t0) t2
case Flat : f:F ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Flat f) t t0) t2)→(eq T (THead (Flat f) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat f) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat f) t t0) t2
we proceed by induction on f to prove
or
∀t2:T.(pr0 (THead (Flat f) t t0) t2)→(eq T (THead (Flat f) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat f) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat f) t t0) t2
case Appl : ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
(H_x)
by (binder_dec .)
or
ex_3 B T T λb:B.λw:T.λu:T.eq T t0 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t0 (THead (Bind b) w u))→∀P:Prop.P
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
case or_introl : H2:ex_3 B T T λb:B.λw:T.λu:T.eq T t0 (THead (Bind b) w u) ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
we proceed by induction on H2 to prove
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
case ex_3_intro : x0:B x1:T x2:T H3:eq T t0 (THead (Bind x0) x1 x2) ⇒
the thesis becomes
or
∀t3:T.(pr0 (THead (Flat Appl) t t0) t3)→(eq T (THead (Flat Appl) t t0) t3)
ex2
T
λt3:T.(eq T (THead (Flat Appl) t t0) t3)→∀P:Prop.P
λt3:T.pr0 (THead (Flat Appl) t t0) t3
(H4)
we proceed by induction on H3 to prove
or
∀t3:T.(pr0 (THead (Bind x0) x1 x2) t3)→(eq T (THead (Bind x0) x1 x2) t3)
ex2
T
λt3:T.(eq T (THead (Bind x0) x1 x2) t3)→∀P:Prop.P
λt3:T.pr0 (THead (Bind x0) x1 x2) t3
case refl_equal : ⇒
the thesis becomes the hypothesis H0
or
∀t3:T.(pr0 (THead (Bind x0) x1 x2) t3)→(eq T (THead (Bind x0) x1 x2) t3)
ex2
T
λt3:T.(eq T (THead (Bind x0) x1 x2) t3)→∀P:Prop.P
λt3:T.pr0 (THead (Bind x0) x1 x2) t3
end of H4
suppose :
or
∀t2:T.(pr0 (THead (Bind Abbr) x1 x2) t2)→(eq T (THead (Bind Abbr) x1 x2) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abbr) x1 x2) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abbr) x1 x2) t2
(h1)
suppose H6:
eq
T
THead (Flat Appl) t (THead (Bind Abbr) x1 x2)
THead (Bind Abbr) x1 (THead (Flat Appl) (lift (S O) O t) x2)
assume P: Prop
(H7)
we proceed by induction on H6 to prove
<λ:T.Prop>
CASE THead (Bind Abbr) x1 (THead (Flat Appl) (lift (S O) O t) x2) OF
TSort ⇒False
| TLRef ⇒False
| THead t2⇒
<λ:T.Prop>
CASE t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒True | Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) t (THead (Bind Abbr) x1 x2) OF
TSort ⇒False
| TLRef ⇒False
| THead t2⇒
<λ:T.Prop>
CASE t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒True | Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) t (THead (Bind Abbr) x1 x2) OF
TSort ⇒False
| TLRef ⇒False
| THead t2⇒
<λ:T.Prop>
CASE t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Bind Abbr) x1 (THead (Flat Appl) (lift (S O) O t) x2) OF
TSort ⇒False
| TLRef ⇒False
| THead t2⇒
<λ:T.Prop>
CASE t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒True | Flat ⇒False
end of H7
consider H7
we proved
<λ:T.Prop>
CASE THead (Bind Abbr) x1 (THead (Flat Appl) (lift (S O) O t) x2) OF
TSort ⇒False
| TLRef ⇒False
| THead t2⇒
<λ:T.Prop>
CASE t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒True | Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
(eq
T
THead (Flat Appl) t (THead (Bind Abbr) x1 x2)
THead (Bind Abbr) x1 (THead (Flat Appl) (lift (S O) O t) x2))
→∀P:Prop.P
end of h1
(h2)
(h1) by (pr0_refl .) we proved pr0 t t
(h2) by (pr0_refl .) we proved pr0 x1 x1
(h3) by (pr0_refl .) we proved pr0 x2 x2
by (pr0_upsilon . not_abbr_abst . . h1 . . h2 . . h3)
pr0
THead (Flat Appl) t (THead (Bind Abbr) x1 x2)
THead (Bind Abbr) x1 (THead (Flat Appl) (lift (S O) O t) x2)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T
.eq T (THead (Flat Appl) t (THead (Bind Abbr) x1 x2)) t2
→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t (THead (Bind Abbr) x1 x2)) t2
by (or_intror . . previous)
we proved
or
∀t2:T
.pr0 (THead (Flat Appl) t (THead (Bind Abbr) x1 x2)) t2
→eq T (THead (Flat Appl) t (THead (Bind Abbr) x1 x2)) t2
ex2
T
λt2:T
.eq T (THead (Flat Appl) t (THead (Bind Abbr) x1 x2)) t2
→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t (THead (Bind Abbr) x1 x2)) t2
(or
∀t2:T.(pr0 (THead (Bind Abbr) x1 x2) t2)→(eq T (THead (Bind Abbr) x1 x2) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abbr) x1 x2) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abbr) x1 x2) t2)
→(or
∀t2:T
.pr0 (THead (Flat Appl) t (THead (Bind Abbr) x1 x2)) t2
→eq T (THead (Flat Appl) t (THead (Bind Abbr) x1 x2)) t2
ex2
T
λt2:T
.eq T (THead (Flat Appl) t (THead (Bind Abbr) x1 x2)) t2
→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t (THead (Bind Abbr) x1 x2)) t2)
suppose :
or
∀t2:T.(pr0 (THead (Bind Abst) x1 x2) t2)→(eq T (THead (Bind Abst) x1 x2) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) x1 x2) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) x1 x2) t2
(h1)
suppose H6:
eq
T
THead (Flat Appl) t (THead (Bind Abst) x1 x2)
THead (Bind Abbr) t x2
assume P: Prop
(H7)
we proceed by induction on H6 to prove
<λ:T.Prop>
CASE THead (Bind Abbr) t x2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) t (THead (Bind Abst) x1 x2) OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) t (THead (Bind Abst) x1 x2) OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind Abbr) t x2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
end of H7
consider H7
we proved
<λ:T.Prop>
CASE THead (Bind Abbr) t x2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
(eq
T
THead (Flat Appl) t (THead (Bind Abst) x1 x2)
THead (Bind Abbr) t x2)
→∀P:Prop.P
end of h1
(h2)
(h1) by (pr0_refl .) we proved pr0 t t
(h2) by (pr0_refl .) we proved pr0 x2 x2
by (pr0_beta . . . h1 . . h2)
pr0
THead (Flat Appl) t (THead (Bind Abst) x1 x2)
THead (Bind Abbr) t x2
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T
.eq T (THead (Flat Appl) t (THead (Bind Abst) x1 x2)) t2
→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t (THead (Bind Abst) x1 x2)) t2
by (or_intror . . previous)
we proved
or
∀t2:T
.pr0 (THead (Flat Appl) t (THead (Bind Abst) x1 x2)) t2
→eq T (THead (Flat Appl) t (THead (Bind Abst) x1 x2)) t2
ex2
T
λt2:T
.eq T (THead (Flat Appl) t (THead (Bind Abst) x1 x2)) t2
→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t (THead (Bind Abst) x1 x2)) t2
(or
∀t2:T.(pr0 (THead (Bind Abst) x1 x2) t2)→(eq T (THead (Bind Abst) x1 x2) t2)
ex2
T
λt2:T.(eq T (THead (Bind Abst) x1 x2) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Abst) x1 x2) t2)
→(or
∀t2:T
.pr0 (THead (Flat Appl) t (THead (Bind Abst) x1 x2)) t2
→eq T (THead (Flat Appl) t (THead (Bind Abst) x1 x2)) t2
ex2
T
λt2:T
.eq T (THead (Flat Appl) t (THead (Bind Abst) x1 x2)) t2
→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t (THead (Bind Abst) x1 x2)) t2)
suppose :
or
∀t2:T.(pr0 (THead (Bind Void) x1 x2) t2)→(eq T (THead (Bind Void) x1 x2) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) x1 x2) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) x1 x2) t2
(h1)
suppose H6:
eq
T
THead (Flat Appl) t (THead (Bind Void) x1 x2)
THead (Bind Void) x1 (THead (Flat Appl) (lift (S O) O t) x2)
assume P: Prop
(H7)
we proceed by induction on H6 to prove
<λ:T.Prop>
CASE THead (Bind Void) x1 (THead (Flat Appl) (lift (S O) O t) x2) OF
TSort ⇒False
| TLRef ⇒False
| THead t2⇒
<λ:T.Prop>
CASE t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒True | Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) t (THead (Bind Void) x1 x2) OF
TSort ⇒False
| TLRef ⇒False
| THead t2⇒
<λ:T.Prop>
CASE t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒True | Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) t (THead (Bind Void) x1 x2) OF
TSort ⇒False
| TLRef ⇒False
| THead t2⇒
<λ:T.Prop>
CASE t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Bind Void) x1 (THead (Flat Appl) (lift (S O) O t) x2) OF
TSort ⇒False
| TLRef ⇒False
| THead t2⇒
<λ:T.Prop>
CASE t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒True | Flat ⇒False
end of H7
consider H7
we proved
<λ:T.Prop>
CASE THead (Bind Void) x1 (THead (Flat Appl) (lift (S O) O t) x2) OF
TSort ⇒False
| TLRef ⇒False
| THead t2⇒
<λ:T.Prop>
CASE t2 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒True | Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
(eq
T
THead (Flat Appl) t (THead (Bind Void) x1 x2)
THead (Bind Void) x1 (THead (Flat Appl) (lift (S O) O t) x2))
→∀P:Prop.P
end of h1
(h2)
(h1)
by (sym_not_eq . . . not_abst_void)
not (eq B Void Abst)
end of h1
(h2) by (pr0_refl .) we proved pr0 t t
(h3) by (pr0_refl .) we proved pr0 x1 x1
(h4) by (pr0_refl .) we proved pr0 x2 x2
by (pr0_upsilon . h1 . . h2 . . h3 . . h4)
pr0
THead (Flat Appl) t (THead (Bind Void) x1 x2)
THead (Bind Void) x1 (THead (Flat Appl) (lift (S O) O t) x2)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T
.eq T (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2
→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2
by (or_intror . . previous)
we proved
or
∀t2:T
.pr0 (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2
→eq T (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2
ex2
T
λt2:T
.eq T (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2
→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2
(or
∀t2:T.(pr0 (THead (Bind Void) x1 x2) t2)→(eq T (THead (Bind Void) x1 x2) t2)
ex2
T
λt2:T.(eq T (THead (Bind Void) x1 x2) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Bind Void) x1 x2) t2)
→(or
∀t2:T
.pr0 (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2
→eq T (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2
ex2
T
λt2:T
.eq T (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2
→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2)
by (previous . H4)
we proved
or
∀t2:T
.pr0 (THead (Flat Appl) t (THead (Bind x0) x1 x2)) t2
→eq T (THead (Flat Appl) t (THead (Bind x0) x1 x2)) t2
ex2
T
λt2:T.(eq T (THead (Flat Appl) t (THead (Bind x0) x1 x2)) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t (THead (Bind x0) x1 x2)) t2
by (eq_ind_r . . . previous . H3)
or
∀t3:T.(pr0 (THead (Flat Appl) t t0) t3)→(eq T (THead (Flat Appl) t t0) t3)
ex2
T
λt3:T.(eq T (THead (Flat Appl) t t0) t3)→∀P:Prop.P
λt3:T.pr0 (THead (Flat Appl) t t0) t3
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
case or_intror : H2:∀b:B.∀w:T.∀u:T.(eq T t0 (THead (Bind b) w u))→∀P:Prop.P ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
(H3) consider H
we proceed by induction on H3 to prove
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
case or_introl : H4:∀t2:T.(pr0 t t2)→(eq T t t2) ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
(H5) consider H0
we proceed by induction on H5 to prove
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
case or_introl : H6:∀t2:T.(pr0 t0 t2)→(eq T t0 t2) ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
assume t2: T
suppose H7: pr0 (THead (Flat Appl) t t0) t2
by (pr0_gen_appl . . . H7)
we proved
or3
ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr0 t u2 λ:T.λt2:T.pr0 t0 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T t0 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T t2 (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr0 t u2
λ:T.λz1:T.λ:T.λt2:T.pr0 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 t0 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λu2:T
.λv2:T
.λt2:T.eq T t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))
λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 t u2
λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2
λ:B.λ:T.λz1:T.λ:T.λ:T.λt2:T.pr0 z1 t2
we proceed by induction on the previous result to prove eq T (THead (Flat Appl) t t0) t2
case or3_intro0 : H8:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr0 t u2 λ:T.λt3:T.pr0 t0 t3 ⇒
the thesis becomes eq T (THead (Flat Appl) t t0) t2
we proceed by induction on H8 to prove eq T (THead (Flat Appl) t t0) t2
case ex3_2_intro : x0:T x1:T H9:eq T t2 (THead (Flat Appl) x0 x1) H10:pr0 t x0 H11:pr0 t0 x1 ⇒
the thesis becomes eq T (THead (Flat Appl) t t0) t2
(H_y) by (H6 . H11) we proved eq T t0 x1
(H_y0) by (H4 . H10) we proved eq T t x0
(H13)
by (eq_ind_r . . . H9 . H_y)
eq T t2 (THead (Flat Appl) x0 t0)
end of H13
(H15)
by (eq_ind_r . . . H13 . H_y0)
eq T t2 (THead (Flat Appl) t t0)
end of H15
by (refl_equal . .)
we proved eq T (THead (Flat Appl) t t0) (THead (Flat Appl) t t0)
by (eq_ind_r . . . previous . H15)
eq T (THead (Flat Appl) t t0) t2
eq T (THead (Flat Appl) t t0) t2
case or3_intro1 : H8:ex4_4 T T T T λy1:T.λz1:T.λ:T.λ:T.eq T t0 (THead (Bind Abst) y1 z1) λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3) λ:T.λ:T.λu2:T.λ:T.pr0 t u2 λ:T.λz1:T.λ:T.λt3:T.pr0 z1 t3 ⇒
the thesis becomes eq T (THead (Flat Appl) t t0) t2
we proceed by induction on H8 to prove eq T (THead (Flat Appl) t t0) t2
case ex4_4_intro : x0:T x1:T x2:T x3:T H9:eq T t0 (THead (Bind Abst) x0 x1) H10:eq T t2 (THead (Bind Abbr) x2 x3) :pr0 t x2 :pr0 x1 x3 ⇒
the thesis becomes eq T (THead (Flat Appl) t t0) t2
(H13)
we proceed by induction on H9 to prove ∀t4:T.(pr0 (THead (Bind Abst) x0 x1) t4)→(eq T (THead (Bind Abst) x0 x1) t4)
case refl_equal : ⇒
the thesis becomes the hypothesis H6
∀t4:T.(pr0 (THead (Bind Abst) x0 x1) t4)→(eq T (THead (Bind Abst) x0 x1) t4)
end of H13
(H14)
we proceed by induction on H9 to prove
∀b:B
.∀w:T
.∀u:T
.(eq T (THead (Bind Abst) x0 x1) (THead (Bind b) w u))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀b:B
.∀w:T
.∀u:T
.(eq T (THead (Bind Abst) x0 x1) (THead (Bind b) w u))→∀P:Prop.P
end of H14
by (pr0_refl .)
we proved pr0 (THead (Bind Abst) x0 x1) (THead (Bind Abst) x0 x1)
by (H13 . previous)
we proved eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) x0 x1)
by (H14 . . . previous .)
we proved
eq
T
THead (Flat Appl) t (THead (Bind Abst) x0 x1)
THead (Bind Abbr) x2 x3
by (eq_ind_r . . . previous . H9)
we proved eq T (THead (Flat Appl) t t0) (THead (Bind Abbr) x2 x3)
by (eq_ind_r . . . previous . H10)
eq T (THead (Flat Appl) t t0) t2
eq T (THead (Flat Appl) t t0) t2
case or3_intro2 : H8: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 t0 (THead (Bind b) y1 z1) λb:B.λ:T.λ:T.λu2:T.λv2:T.λt3:T.eq T t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t3)) λ:B.λ:T.λ:T.λu2:T.λ:T.λ:T.pr0 t u2 λ:B.λy1:T.λ:T.λ:T.λv2:T.λ:T.pr0 y1 v2 λ:B.λ:T.λz1:T.λ:T.λ:T.λt3:T.pr0 z1 t3 ⇒
the thesis becomes eq T (THead (Flat Appl) t t0) t2
we proceed by induction on H8 to prove eq T (THead (Flat Appl) t t0) t2
case ex6_6_intro : x0:B x1:T x2:T x3:T x4:T x5:T :not (eq B x0 Abst) H10:eq T t0 (THead (Bind x0) x1 x2) H11:eq T t2 (THead (Bind x0) x4 (THead (Flat Appl) (lift (S O) O x3) x5)) :pr0 t x3 :pr0 x1 x4 :pr0 x2 x5 ⇒
the thesis becomes eq T (THead (Flat Appl) t t0) t2
(H15)
we proceed by induction on H10 to prove ∀t4:T.(pr0 (THead (Bind x0) x1 x2) t4)→(eq T (THead (Bind x0) x1 x2) t4)
case refl_equal : ⇒
the thesis becomes the hypothesis H6
∀t4:T.(pr0 (THead (Bind x0) x1 x2) t4)→(eq T (THead (Bind x0) x1 x2) t4)
end of H15
(H16)
we proceed by induction on H10 to prove
∀b:B
.∀w:T.∀u:T.(eq T (THead (Bind x0) x1 x2) (THead (Bind b) w u))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀b:B
.∀w:T.∀u:T.(eq T (THead (Bind x0) x1 x2) (THead (Bind b) w u))→∀P:Prop.P
end of H16
by (pr0_refl .)
we proved pr0 (THead (Bind x0) x1 x2) (THead (Bind x0) x1 x2)
by (H15 . previous)
we proved eq T (THead (Bind x0) x1 x2) (THead (Bind x0) x1 x2)
by (H16 . . . previous .)
we proved
eq
T
THead (Flat Appl) t (THead (Bind x0) x1 x2)
THead (Bind x0) x4 (THead (Flat Appl) (lift (S O) O x3) x5)
by (eq_ind_r . . . previous . H10)
we proved
eq
T
THead (Flat Appl) t t0
THead (Bind x0) x4 (THead (Flat Appl) (lift (S O) O x3) x5)
by (eq_ind_r . . . previous . H11)
eq T (THead (Flat Appl) t t0) t2
eq T (THead (Flat Appl) t t0) t2
we proved eq T (THead (Flat Appl) t t0) t2
we proved
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
by (or_introl . . previous)
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
case or_intror : H6:ex2 T λt2:T.(eq T t0 t2)→∀P:Prop.P λt2:T.pr0 t0 t2 ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
we proceed by induction on H6 to prove
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
case ex_intro2 : x:T H7:(eq T t0 x)→∀P:Prop.P H8:pr0 t0 x ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
(h1)
suppose H9: eq T (THead (Flat Appl) t t0) (THead (Flat Appl) t x)
assume P: Prop
(H10)
by (f_equal . . . . . H9)
we proved
eq
T
<λ:T.T> CASE THead (Flat Appl) t t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
<λ:T.T> CASE THead (Flat Appl) t x OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
THead (Flat Appl) t t0
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
THead (Flat Appl) t x
end of H10
(H12)
consider H10
we proved
eq
T
<λ:T.T> CASE THead (Flat Appl) t t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
<λ:T.T> CASE THead (Flat Appl) t x OF TSort ⇒t0 | TLRef ⇒t0 | THead t2⇒t2
that is equivalent to eq T t0 x
by (eq_ind_r . . . H7 . previous)
(eq T t0 t0)→∀P0:Prop.P0
end of H12
by (refl_equal . .)
we proved eq T t0 t0
by (H12 previous .)
we proved P
eq T (THead (Flat Appl) t t0) (THead (Flat Appl) t x)
→∀P:Prop.P
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t t
by (pr0_comp . . previous . . H8 .)
pr0 (THead (Flat Appl) t t0) (THead (Flat Appl) t x)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
by (or_intror . . previous)
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
case or_intror : H4:ex2 T λt2:T.(eq T t t2)→∀P:Prop.P λt2:T.pr0 t t2 ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
we proceed by induction on H4 to prove
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
case ex_intro2 : x:T H5:(eq T t x)→∀P:Prop.P H6:pr0 t x ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
(h1)
suppose H7: eq T (THead (Flat Appl) t t0) (THead (Flat Appl) x t0)
assume P: Prop
(H8)
by (f_equal . . . . . H7)
we proved
eq
T
<λ:T.T> CASE THead (Flat Appl) t t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
<λ:T.T> CASE THead (Flat Appl) x t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
THead (Flat Appl) t t0
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
THead (Flat Appl) x t0
end of H8
(H10)
consider H8
we proved
eq
T
<λ:T.T> CASE THead (Flat Appl) t t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
<λ:T.T> CASE THead (Flat Appl) x t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
that is equivalent to eq T t x
by (eq_ind_r . . . H5 . previous)
(eq T t t)→∀P0:Prop.P0
end of H10
by (refl_equal . .)
we proved eq T t t
by (H10 previous .)
we proved P
eq T (THead (Flat Appl) t t0) (THead (Flat Appl) x t0)
→∀P:Prop.P
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t0 t0
by (pr0_comp . . H6 . . previous .)
pr0 (THead (Flat Appl) t t0) (THead (Flat Appl) x t0)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
by (or_intror . . previous)
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
or
∀t2:T.(pr0 (THead (Flat Appl) t t0) t2)→(eq T (THead (Flat Appl) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Appl) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Appl) t t0) t2
case Cast : ⇒
the thesis becomes
or
∀t2:T.(pr0 (THead (Flat Cast) t t0) t2)→(eq T (THead (Flat Cast) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Cast) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Cast) t t0) t2
(h1)
suppose H1: eq T (THead (Flat Cast) t t0) t0
assume P: Prop
by (thead_x_y_y . . . H1 .)
we proved P
(eq T (THead (Flat Cast) t t0) t0)→∀P:Prop.P
end of h1
(h2)
by (pr0_refl .)
we proved pr0 t0 t0
by (pr0_tau . . previous .)
pr0 (THead (Flat Cast) t t0) t0
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
T
λt2:T.(eq T (THead (Flat Cast) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Cast) t t0) t2
by (or_intror . . previous)
or
∀t2:T.(pr0 (THead (Flat Cast) t t0) t2)→(eq T (THead (Flat Cast) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat Cast) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat Cast) t t0) t2
or
∀t2:T.(pr0 (THead (Flat f) t t0) t2)→(eq T (THead (Flat f) t t0) t2)
ex2
T
λt2:T.(eq T (THead (Flat f) t t0) t2)→∀P:Prop.P
λt2:T.pr0 (THead (Flat f) t t0) t2
or
∀t2:T.(pr0 (THead k t t0) t2)→(eq T (THead k t t0) t2)
ex2 T λt2:T.(eq T (THead k t t0) t2)→∀P:Prop.P λt2:T.pr0 (THead k t t0) t2
we proved 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)
we proved ∀t1:T.(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))