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