DEFINITION sn3_beta()
TYPE =
∀c:C
.∀v:T
.∀t:T
.sn3 c (THead (Bind Abbr) v t)
→∀w:T
.(sn3 c w)→(sn3 c (THead (Flat Appl) v (THead (Bind Abst) w t)))
BODY =
assume c: C
assume v: T
assume t: T
suppose H: sn3 c (THead (Bind Abbr) v t)
assume y: T
suppose H0: sn3 c y
we proceed by induction on H0 to prove
∀x:T
.∀x0:T
.eq T y (THead (Bind Abbr) x x0)
→∀w:T
.(sn3 c w)→(sn3 c (THead (Flat Appl) x (THead (Bind Abst) w x0)))
case sn3_sing : t1:T H1:∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(sn3 c t2) ⇒
the thesis becomes
∀x:T
.∀x0:T
.∀H3:eq T t1 (THead (Bind Abbr) x x0)
.∀w:T.∀H4:(sn3 c w).(sn3 c (THead (Flat Appl) x (THead (Bind Abst) w x0)))
(H2) by induction hypothesis we know
∀t2:T
.(eq T t1 t2)→∀P:Prop.P
→(pr3 c t1 t2
→∀x:T
.∀x0:T
.eq T t2 (THead (Bind Abbr) x x0)
→∀w:T
.(sn3 c w)→(sn3 c (THead (Flat Appl) x (THead (Bind Abst) w x0))))
assume x: T
assume x0: T
suppose H3: eq T t1 (THead (Bind Abbr) x x0)
assume w: T
suppose H4: sn3 c w
(H5)
we proceed by induction on H3 to prove
∀t2:T
.(eq T (THead (Bind Abbr) x x0) t2)→∀P:Prop.P
→(pr3 c (THead (Bind Abbr) x x0) t2
→∀x1:T
.∀x2:T
.eq T t2 (THead (Bind Abbr) x1 x2)
→∀w0:T.(sn3 c w0)→(sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) w0 x2))))
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀t2:T
.(eq T (THead (Bind Abbr) x x0) t2)→∀P:Prop.P
→(pr3 c (THead (Bind Abbr) x x0) t2
→∀x1:T
.∀x2:T
.eq T t2 (THead (Bind Abbr) x1 x2)
→∀w0:T.(sn3 c w0)→(sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) w0 x2))))
end of H5
(H6)
we proceed by induction on H3 to prove
∀t2:T
.(eq T (THead (Bind Abbr) x x0) t2)→∀P:Prop.P
→(pr3 c (THead (Bind Abbr) x x0) t2)→(sn3 c t2)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
∀t2:T
.(eq T (THead (Bind Abbr) x x0) t2)→∀P:Prop.P
→(pr3 c (THead (Bind Abbr) x x0) t2)→(sn3 c t2)
end of H6
we proceed by induction on H4 to prove sn3 c (THead (Flat Appl) x (THead (Bind Abst) w x0))
case sn3_sing : t2:T H7:∀t3:T.((eq T t2 t3)→∀P:Prop.P)→(pr3 c t2 t3)→(sn3 c t3) ⇒
the thesis becomes sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x0))
(H8) by induction hypothesis we know
∀t3:T
.(eq T t2 t3)→∀P:Prop.P
→(pr3 c t2 t3)→(sn3 c (THead (Flat Appl) x (THead (Bind Abst) t3 x0)))
assume t3: T
suppose H9:
eq T (THead (Flat Appl) x (THead (Bind Abst) t2 x0)) t3
→∀P:Prop.P
suppose H10: pr2 c (THead (Flat Appl) x (THead (Bind Abst) t2 x0)) t3
(H11)
by (pr2_gen_appl . . . . H10)
or3
ex3_2
T
T
λu2:T.λt2:T.eq T t3 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr2 c x u2
λ:T.λt2:T.pr2 c (THead (Bind Abst) t2 x0) t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T (THead (Bind Abst) t2 x0) (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T t3 (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr2 c x u2
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (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 (THead (Bind Abst) t2 x0) (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T
.λy2:T.eq T t3 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr2 c x u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr2 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr2 (CHead c (Bind b) y2) z1 z2
end of H11
we proceed by induction on H11 to prove sn3 c t3
case or3_intro0 : H12:ex3_2 T T λu2:T.λt4:T.eq T t3 (THead (Flat Appl) u2 t4) λu2:T.λ:T.pr2 c x u2 λ:T.λt4:T.pr2 c (THead (Bind Abst) t2 x0) t4 ⇒
the thesis becomes sn3 c t3
we proceed by induction on H12 to prove sn3 c t3
case ex3_2_intro : x1:T x2:T H13:eq T t3 (THead (Flat Appl) x1 x2) H14:pr2 c x x1 H15:pr2 c (THead (Bind Abst) t2 x0) x2 ⇒
the thesis becomes sn3 c t3
(H16)
we proceed by induction on H13 to prove
(eq
T
THead (Flat Appl) x (THead (Bind Abst) t2 x0)
THead (Flat Appl) x1 x2)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H9
(eq
T
THead (Flat Appl) x (THead (Bind Abst) t2 x0)
THead (Flat Appl) x1 x2)
→∀P:Prop.P
end of H16
(H17)
by (pr2_gen_abst . . . . H15)
ex3_2
T
T
λu2:T.λt2:T.eq T x2 (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr2 c t2 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x0 t2)
end of H17
we proceed by induction on H17 to prove sn3 c (THead (Flat Appl) x1 x2)
case ex3_2_intro : x3:T x4:T H18:eq T x2 (THead (Bind Abst) x3 x4) H19:pr2 c t2 x3 H20:∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x0 x4) ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 x2)
(H21)
we proceed by induction on H18 to prove
(eq
T
THead (Flat Appl) x (THead (Bind Abst) t2 x0)
THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H16
(eq
T
THead (Flat Appl) x (THead (Bind Abst) t2 x0)
THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
→∀P:Prop.P
end of H21
(H_x)
by (term_dec . .)
or (eq T t2 x3) (eq T t2 x3)→∀P:Prop.P
end of H_x
(H22) consider H_x
we proceed by induction on H22 to prove sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
case or_introl : H23:eq T t2 x3 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
(H24)
by (eq_ind_r . . . H21 . H23)
(eq
T
THead (Flat Appl) x (THead (Bind Abst) t2 x0)
THead (Flat Appl) x1 (THead (Bind Abst) t2 x4))
→∀P:Prop.P
end of H24
we proceed by induction on H23 to prove sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) t2 x4))
(H_x0)
by (term_dec . .)
or (eq T x x1) (eq T x x1)→∀P:Prop.P
end of H_x0
(H26) consider H_x0
we proceed by induction on H26 to prove sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) t2 x4))
case or_introl : H27:eq T x x1 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) t2 x4))
(H28)
by (eq_ind_r . . . H24 . H27)
(eq
T
THead (Flat Appl) x (THead (Bind Abst) t2 x0)
THead (Flat Appl) x (THead (Bind Abst) t2 x4))
→∀P:Prop.P
end of H28
we proceed by induction on H27 to prove sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) t2 x4))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x4))
(H_x1)
by (term_dec . .)
or (eq T x0 x4) (eq T x0 x4)→∀P:Prop.P
end of H_x1
(H30) consider H_x1
we proceed by induction on H30 to prove sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x4))
case or_introl : H31:eq T x0 x4 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x4))
(H32)
by (eq_ind_r . . . H28 . H31)
(eq
T
THead (Flat Appl) x (THead (Bind Abst) t2 x0)
THead (Flat Appl) x (THead (Bind Abst) t2 x0))
→∀P:Prop.P
end of H32
we proceed by induction on H31 to prove sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x4))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x0))
by (refl_equal . .)
we proved
eq
T
THead (Flat Appl) x (THead (Bind Abst) t2 x0)
THead (Flat Appl) x (THead (Bind Abst) t2 x0)
by (H32 previous .)
sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x0))
sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x4))
case or_intror : H31:(eq T x0 x4)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x4))
(h1)
suppose H32: eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
assume P: Prop
(H33)
by (f_equal . . . . . H32)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abbr) x x4 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abbr) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abbr) x x4
end of H33
(H34)
consider H33
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abbr) x x4 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
that is equivalent to eq T x0 x4
by (eq_ind_r . . . H31 . previous)
(eq T x0 x0)→∀P0:Prop.P0
end of H34
by (refl_equal . .)
we proved eq T x0 x0
by (H34 previous .)
we proved P
eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
→∀P:Prop.P
end of h1
(h2)
by (H20 . .)
we proved pr2 (CHead c (Bind Abbr) x) x0 x4
by (pr2_head_2 . . . . . previous)
we proved pr2 c (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
by (pr3_pr2 . . . previous)
pr3 c (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
end of h2
(h3)
by (refl_equal . .)
eq T (THead (Bind Abbr) x x4) (THead (Bind Abbr) x x4)
end of h3
(h4) by (sn3_sing . . H7) we proved sn3 c t2
by (H5 . h1 h2 . . h3 . h4)
sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x4))
sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x4))
sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) t2 x4))
case or_intror : H27:(eq T x x1)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) t2 x4))
(h1)
suppose H28: eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr) x1 x4)
assume P: Prop
(H29)
by (f_equal . . . . . H28)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abbr) x1 x4 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
THead (Bind Abbr) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
THead (Bind Abbr) x1 x4
end of H29
(h1)
(H30)
by (f_equal . . . . . H28)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abbr) x1 x4 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abbr) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abbr) x1 x4
end of H30
suppose H31: eq T x x1
(H33)
by (eq_ind_r . . . H27 . H31)
(eq T x x)→∀P0:Prop.P0
end of H33
by (refl_equal . .)
we proved eq T x x
by (H33 previous .)
we proved P
(eq T x x1)→P
end of h1
(h2)
consider H29
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abbr) x1 x4 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
eq T x x1
end of h2
by (h1 h2)
we proved P
eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr) x1 x4)
→∀P:Prop.P
end of h1
(h2)
(h1) by (pr3_pr2 . . . H14) we proved pr3 c x x1
(h2)
by (H20 . .)
we proved pr2 (CHead c (Bind Abbr) x1) x0 x4
by (pr3_pr2 . . . previous)
pr3 (CHead c (Bind Abbr) x1) x0 x4
end of h2
by (pr3_head_12 . . . h1 . . . h2)
pr3 c (THead (Bind Abbr) x x0) (THead (Bind Abbr) x1 x4)
end of h2
(h3)
by (refl_equal . .)
eq T (THead (Bind Abbr) x1 x4) (THead (Bind Abbr) x1 x4)
end of h3
(h4) by (sn3_sing . . H7) we proved sn3 c t2
by (H5 . h1 h2 . . h3 . h4)
sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) t2 x4))
sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) t2 x4))
sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
case or_intror : H23:(eq T t2 x3)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
(H_x0)
by (term_dec . .)
or (eq T x x1) (eq T x x1)→∀P:Prop.P
end of H_x0
(H24) consider H_x0
we proceed by induction on H24 to prove sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
case or_introl : H25:eq T x x1 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
we proceed by induction on H25 to prove sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
(H_x1)
by (term_dec . .)
or (eq T x0 x4) (eq T x0 x4)→∀P:Prop.P
end of H_x1
(H27) consider H_x1
we proceed by induction on H27 to prove sn3 c (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
case or_introl : H28:eq T x0 x4 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
we proceed by induction on H28 to prove sn3 c (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x (THead (Bind Abst) x3 x0))
by (pr3_pr2 . . . H19)
we proved pr3 c t2 x3
by (H8 . H23 previous)
sn3 c (THead (Flat Appl) x (THead (Bind Abst) x3 x0))
sn3 c (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
case or_intror : H28:(eq T x0 x4)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
(h1)
suppose H29: eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
assume P: Prop
(H30)
by (f_equal . . . . . H29)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abbr) x x4 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abbr) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abbr) x x4
end of H30
(H31)
consider H30
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abbr) x x4 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
that is equivalent to eq T x0 x4
by (eq_ind_r . . . H28 . previous)
(eq T x0 x0)→∀P0:Prop.P0
end of H31
by (refl_equal . .)
we proved eq T x0 x0
by (H31 previous .)
we proved P
eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
→∀P:Prop.P
end of h1
(h2)
by (H20 . .)
we proved pr2 (CHead c (Bind Abbr) x) x0 x4
by (pr2_head_2 . . . . . previous)
we proved pr2 c (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
by (pr3_pr2 . . . previous)
pr3 c (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
end of h2
(h3)
by (refl_equal . .)
eq T (THead (Bind Abbr) x x4) (THead (Bind Abbr) x x4)
end of h3
(h4)
by (pr3_pr2 . . . H19)
we proved pr3 c t2 x3
by (H7 . H23 previous)
sn3 c x3
end of h4
by (H5 . h1 h2 . . h3 . h4)
sn3 c (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
sn3 c (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
case or_intror : H25:(eq T x x1)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
(h1)
suppose H26: eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr) x1 x4)
assume P: Prop
(H27)
by (f_equal . . . . . H26)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abbr) x1 x4 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
THead (Bind Abbr) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
THead (Bind Abbr) x1 x4
end of H27
(h1)
(H28)
by (f_equal . . . . . H26)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abbr) x1 x4 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abbr) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abbr) x1 x4
end of H28
suppose H29: eq T x x1
(H31)
by (eq_ind_r . . . H25 . H29)
(eq T x x)→∀P0:Prop.P0
end of H31
by (refl_equal . .)
we proved eq T x x
by (H31 previous .)
we proved P
(eq T x x1)→P
end of h1
(h2)
consider H27
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abbr) x1 x4 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
eq T x x1
end of h2
by (h1 h2)
we proved P
eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr) x1 x4)
→∀P:Prop.P
end of h1
(h2)
(h1) by (pr3_pr2 . . . H14) we proved pr3 c x x1
(h2)
by (H20 . .)
we proved pr2 (CHead c (Bind Abbr) x1) x0 x4
by (pr3_pr2 . . . previous)
pr3 (CHead c (Bind Abbr) x1) x0 x4
end of h2
by (pr3_head_12 . . . h1 . . . h2)
pr3 c (THead (Bind Abbr) x x0) (THead (Bind Abbr) x1 x4)
end of h2
(h3)
by (refl_equal . .)
eq T (THead (Bind Abbr) x1 x4) (THead (Bind Abbr) x1 x4)
end of h3
(h4)
by (pr3_pr2 . . . H19)
we proved pr3 c t2 x3
by (H7 . H23 previous)
sn3 c x3
end of h4
by (H5 . h1 h2 . . h3 . h4)
sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
we proved sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))
by (eq_ind_r . . . previous . H18)
sn3 c (THead (Flat Appl) x1 x2)
we proved sn3 c (THead (Flat Appl) x1 x2)
by (eq_ind_r . . . previous . H13)
sn3 c t3
sn3 c t3
case or3_intro1 : H12:ex4_4 T T T T λy1:T.λz1:T.λ:T.λ:T.eq T (THead (Bind Abst) t2 x0) (THead (Bind Abst) y1 z1) λ:T.λ:T.λu2:T.λt4:T.eq T t3 (THead (Bind Abbr) u2 t4) λ:T.λ:T.λu2:T.λ:T.pr2 c x u2 λ:T.λz1:T.λ:T.λt4:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) z1 t4) ⇒
the thesis becomes sn3 c t3
we proceed by induction on H12 to prove sn3 c t3
case ex4_4_intro : x1:T x2:T x3:T x4:T H13:eq T (THead (Bind Abst) t2 x0) (THead (Bind Abst) x1 x2) H14:eq T t3 (THead (Bind Abbr) x3 x4) H15:pr2 c x x3 H16:∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x2 x4) ⇒
the thesis becomes sn3 c t3
(H18)
by (f_equal . . . . . H13)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t2 x0 OF TSort ⇒t2 | TLRef ⇒t2 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abst) x1 x2 OF TSort ⇒t2 | TLRef ⇒t2 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t2 | TLRef ⇒t2 | THead t0 ⇒t0
THead (Bind Abst) t2 x0
λe:T.<λ:T.T> CASE e OF TSort ⇒t2 | TLRef ⇒t2 | THead t0 ⇒t0
THead (Bind Abst) x1 x2
end of H18
(h1)
(H19)
by (f_equal . . . . . H13)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t2 x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abst) x1 x2 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abst) t2 x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abst) x1 x2
end of H19
suppose : eq T t2 x1
(H21)
consider H19
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t2 x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abst) x1 x2 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
that is equivalent to eq T x0 x2
by (eq_ind_r . . . H16 . previous)
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x0 x4)
end of H21
(H_x)
by (term_dec . .)
or (eq T x x3) (eq T x x3)→∀P:Prop.P
end of H_x
(H22) consider H_x
we proceed by induction on H22 to prove sn3 c (THead (Bind Abbr) x3 x4)
case or_introl : H23:eq T x x3 ⇒
the thesis becomes sn3 c (THead (Bind Abbr) x3 x4)
we proceed by induction on H23 to prove sn3 c (THead (Bind Abbr) x3 x4)
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Bind Abbr) x x4)
(H_x0)
by (term_dec . .)
or (eq T x0 x4) (eq T x0 x4)→∀P:Prop.P
end of H_x0
(H25) consider H_x0
we proceed by induction on H25 to prove sn3 c (THead (Bind Abbr) x x4)
case or_introl : H26:eq T x0 x4 ⇒
the thesis becomes sn3 c (THead (Bind Abbr) x x4)
we proceed by induction on H26 to prove sn3 c (THead (Bind Abbr) x x4)
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Bind Abbr) x x0)
by (sn3_sing . . H6)
sn3 c (THead (Bind Abbr) x x0)
sn3 c (THead (Bind Abbr) x x4)
case or_intror : H26:(eq T x0 x4)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Bind Abbr) x x4)
(h1)
suppose H27: eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
assume P: Prop
(H28)
by (f_equal . . . . . H27)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abbr) x x4 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abbr) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abbr) x x4
end of H28
(H29)
consider H28
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abbr) x x4 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
that is equivalent to eq T x0 x4
by (eq_ind_r . . . H26 . previous)
(eq T x0 x0)→∀P0:Prop.P0
end of H29
by (refl_equal . .)
we proved eq T x0 x0
by (H29 previous .)
we proved P
eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
→∀P:Prop.P
end of h1
(h2)
by (H21 . .)
we proved pr2 (CHead c (Bind Abbr) x) x0 x4
by (pr2_head_2 . . . . . previous)
we proved pr2 c (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
by (pr3_pr2 . . . previous)
pr3 c (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
end of h2
by (H6 . h1 h2)
sn3 c (THead (Bind Abbr) x x4)
sn3 c (THead (Bind Abbr) x x4)
sn3 c (THead (Bind Abbr) x3 x4)
case or_intror : H23:(eq T x x3)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Bind Abbr) x3 x4)
(h1)
suppose H24: eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr) x3 x4)
assume P: Prop
(H25)
by (f_equal . . . . . H24)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abbr) x3 x4 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
THead (Bind Abbr) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
THead (Bind Abbr) x3 x4
end of H25
(h1)
(H26)
by (f_equal . . . . . H24)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abbr) x3 x4 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abbr) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abbr) x3 x4
end of H26
suppose H27: eq T x x3
(H29)
by (eq_ind_r . . . H23 . H27)
(eq T x x)→∀P0:Prop.P0
end of H29
by (refl_equal . .)
we proved eq T x x
by (H29 previous .)
we proved P
(eq T x x3)→P
end of h1
(h2)
consider H25
we proved
eq
T
<λ:T.T> CASE THead (Bind Abbr) x x0 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abbr) x3 x4 OF TSort ⇒x | TLRef ⇒x | THead t0 ⇒t0
eq T x x3
end of h2
by (h1 h2)
we proved P
eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr) x3 x4)
→∀P:Prop.P
end of h1
(h2)
(h1) by (pr3_pr2 . . . H15) we proved pr3 c x x3
(h2)
by (H21 . .)
we proved pr2 (CHead c (Bind Abbr) x3) x0 x4
by (pr3_pr2 . . . previous)
pr3 (CHead c (Bind Abbr) x3) x0 x4
end of h2
by (pr3_head_12 . . . h1 . . . h2)
pr3 c (THead (Bind Abbr) x x0) (THead (Bind Abbr) x3 x4)
end of h2
by (H6 . h1 h2)
sn3 c (THead (Bind Abbr) x3 x4)
we proved sn3 c (THead (Bind Abbr) x3 x4)
(eq T t2 x1)→(sn3 c (THead (Bind Abbr) x3 x4))
end of h1
(h2)
consider H18
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t2 x0 OF TSort ⇒t2 | TLRef ⇒t2 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abst) x1 x2 OF TSort ⇒t2 | TLRef ⇒t2 | THead t0 ⇒t0
eq T t2 x1
end of h2
by (h1 h2)
we proved sn3 c (THead (Bind Abbr) x3 x4)
by (eq_ind_r . . . previous . H14)
sn3 c t3
sn3 c t3
case or3_intro2 : H12: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 (THead (Bind Abst) t2 x0) (THead (Bind b) y1 z1) λb:B.λ:T.λ:T.λz2:T.λu2:T.λy2:T.eq T t3 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr2 c x u2 λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr2 c y1 y2 λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr2 (CHead c (Bind b) y2) z1 z2 ⇒
the thesis becomes sn3 c t3
we proceed by induction on H12 to prove sn3 c t3
case ex6_6_intro : x1:B x2:T x3:T x4:T x5:T x6:T H13:not (eq B x1 Abst) H14:eq T (THead (Bind Abst) t2 x0) (THead (Bind x1) x2 x3) H15:eq T t3 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4)) :pr2 c x x5 H17:pr2 c x2 x6 H18:pr2 (CHead c (Bind x1) x6) x3 x4 ⇒
the thesis becomes sn3 c t3
(H20)
by (f_equal . . . . . H14)
we proved
eq
B
<λ:T.B>
CASE THead (Bind Abst) t2 x0 OF
TSort ⇒Abst
| TLRef ⇒Abst
| THead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:T.B>
CASE THead (Bind x1) x2 x3 OF
TSort ⇒Abst
| TLRef ⇒Abst
| THead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq
B
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒Abst
| TLRef ⇒Abst
| THead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
THead (Bind Abst) t2 x0
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒Abst
| TLRef ⇒Abst
| THead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
THead (Bind x1) x2 x3
end of H20
(h1)
(H21)
by (f_equal . . . . . H14)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t2 x0 OF TSort ⇒t2 | TLRef ⇒t2 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind x1) x2 x3 OF TSort ⇒t2 | TLRef ⇒t2 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t2 | TLRef ⇒t2 | THead t0 ⇒t0
THead (Bind Abst) t2 x0
λe:T.<λ:T.T> CASE e OF TSort ⇒t2 | TLRef ⇒t2 | THead t0 ⇒t0 (THead (Bind x1) x2 x3)
end of H21
(h1)
(H22)
by (f_equal . . . . . H14)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t2 x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind x1) x2 x3 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abst) t2 x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0 (THead (Bind x1) x2 x3)
end of H22
suppose H23: eq T t2 x2
suppose H24: eq B Abst x1
(H25)
consider H22
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t2 x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind x1) x2 x3 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
that is equivalent to eq T x0 x3
by (eq_ind_r . . . H18 . previous)
pr2 (CHead c (Bind x1) x6) x0 x4
end of H25
(H28)
by (eq_ind_r . . . H13 . H24)
not (eq B Abst Abst)
end of H28
we proceed by induction on H24 to prove sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
case refl_equal : ⇒
the thesis becomes
sn3 c (THead (Bind Abst) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
(H29)
by (refl_equal . .)
we proved eq B Abst Abst
by (H28 previous)
we proved False
by cases on the previous result we prove
sn3 c (THead (Bind Abst) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
sn3 c (THead (Bind Abst) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
end of H29
consider H29
sn3 c (THead (Bind Abst) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
we proved sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
eq T t2 x2
→(eq B Abst x1
→sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4)))
end of h1
(h2)
consider H21
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t2 x0 OF TSort ⇒t2 | TLRef ⇒t2 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind x1) x2 x3 OF TSort ⇒t2 | TLRef ⇒t2 | THead t0 ⇒t0
eq T t2 x2
end of h2
by (h1 h2)
eq B Abst x1
→sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
end of h1
(h2)
consider H20
we proved
eq
B
<λ:T.B>
CASE THead (Bind Abst) t2 x0 OF
TSort ⇒Abst
| TLRef ⇒Abst
| THead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
<λ:T.B>
CASE THead (Bind x1) x2 x3 OF
TSort ⇒Abst
| TLRef ⇒Abst
| THead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒Abst
eq B Abst x1
end of h2
by (h1 h2)
we proved sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
by (eq_ind_r . . . previous . H15)
sn3 c t3
sn3 c t3
we proved sn3 c t3
we proved
∀t3:T
.eq T (THead (Flat Appl) x (THead (Bind Abst) t2 x0)) t3
→∀P:Prop.P
→(pr2 c (THead (Flat Appl) x (THead (Bind Abst) t2 x0)) t3)→(sn3 c t3)
by (sn3_pr2_intro . . previous)
sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x0))
we proved sn3 c (THead (Flat Appl) x (THead (Bind Abst) w x0))
∀x:T
.∀x0:T
.∀H3:eq T t1 (THead (Bind Abbr) x x0)
.∀w:T.∀H4:(sn3 c w).(sn3 c (THead (Flat Appl) x (THead (Bind Abst) w x0)))
we proved
∀x:T
.∀x0:T
.eq T y (THead (Bind Abbr) x x0)
→∀w:T
.(sn3 c w)→(sn3 c (THead (Flat Appl) x (THead (Bind Abst) w x0)))
by (unintro . . . previous)
we proved
∀x:T
.eq T y (THead (Bind Abbr) v x)
→∀w:T
.(sn3 c w)→(sn3 c (THead (Flat Appl) v (THead (Bind Abst) w x)))
by (unintro . . . previous)
we proved
eq T y (THead (Bind Abbr) v t)
→∀w:T
.(sn3 c w)→(sn3 c (THead (Flat Appl) v (THead (Bind Abst) w t)))
we proved
∀y:T
.sn3 c y
→(eq T y (THead (Bind Abbr) v t)
→∀w:T
.(sn3 c w)→(sn3 c (THead (Flat Appl) v (THead (Bind Abst) w t))))
by (insert_eq . . . . previous H)
we proved
∀w:T
.(sn3 c w)→(sn3 c (THead (Flat Appl) v (THead (Bind Abst) w t)))
we proved
∀c:C
.∀v:T
.∀t:T
.sn3 c (THead (Bind Abbr) v t)
→∀w:T
.(sn3 c w)→(sn3 c (THead (Flat Appl) v (THead (Bind Abst) w t)))