DEFINITION sn3_appl_appl()
TYPE =
∀v1:T
.∀t1:T
.let u1 := THead (Flat Appl) v1 t1
in ∀c:C
.sn3 c u1
→∀v2:T
.sn3 c v2
→(∀u2:T.(pr3 c u1 u2)→((iso u1 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 u1))
BODY =
assume v1: T
assume t1: T
we must prove
let u1 := THead (Flat Appl) v1 t1
in ∀c:C
.sn3 c u1
→∀v2:T
.sn3 c v2
→(∀u2:T.(pr3 c u1 u2)→((iso u1 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 u1))
or equivalently
∀c:C
.sn3 c (THead (Flat Appl) v1 t1)
→∀v2:T
.sn3 c v2
→(∀u2:T
.pr3 c (THead (Flat Appl) v1 t1) u2
→((iso (THead (Flat Appl) v1 t1) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 (THead (Flat Appl) v1 t1)))
assume c: C
suppose H: sn3 c (THead (Flat Appl) v1 t1)
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)
→∀v2:T
.sn3 c v2
→(∀u2:T
.pr3 c y u2
→((iso y u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 y))
case sn3_sing : t2:T H1:∀t3:T.((eq T t2 t3)→∀P:Prop.P)→(pr3 c t2 t3)→(sn3 c t3) ⇒
the thesis becomes
∀x:T
.∀x0:T
.∀H3:eq T t2 (THead (Flat Appl) x x0)
.∀v2:T
.∀H4:sn3 c v2
.∀u2:T.(pr3 c t2 u2)→((iso t2 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 t2)
(H2) by induction hypothesis we know
∀t3:T
.(eq T t2 t3)→∀P:Prop.P
→(pr3 c t2 t3
→∀x:T
.∀x0:T
.eq T t3 (THead (Flat Appl) x x0)
→∀v2:T
.sn3 c v2
→(∀u2:T.(pr3 c t3 u2)→((iso t3 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 t3)))
assume x: T
assume x0: T
suppose H3: eq T t2 (THead (Flat Appl) x x0)
assume v2: T
suppose H4: sn3 c v2
we proceed by induction on H4 to prove
∀u2:T.(pr3 c t2 u2)→((iso t2 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 t2)
case sn3_sing : t0:T H5:∀t3:T.((eq T t0 t3)→∀P:Prop.P)→(pr3 c t0 t3)→(sn3 c t3) ⇒
the thesis becomes
∀H7:∀u2:T.(pr3 c t2 u2)→((iso t2 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) t0 u2))
.sn3 c (THead (Flat Appl) t0 t2)
(H6) by induction hypothesis we know
∀t3:T
.(eq T t0 t3)→∀P:Prop.P
→(pr3 c t0 t3
→(∀u2:T.(pr3 c t2 u2)→((iso t2 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) t3 u2))
→sn3 c (THead (Flat Appl) t3 t2)))
suppose H7:
∀u2:T.(pr3 c t2 u2)→((iso t2 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) t0 u2))
(H8)
we proceed by induction on H3 to prove
∀u2:T
.pr3 c (THead (Flat Appl) x x0) u2
→((iso (THead (Flat Appl) x x0) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) t0 u2))
case refl_equal : ⇒
the thesis becomes the hypothesis H7
∀u2:T
.pr3 c (THead (Flat Appl) x x0) u2
→((iso (THead (Flat Appl) x x0) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) t0 u2))
end of H8
(H9)
we proceed by induction on H3 to prove
∀t3:T
.(eq T t0 t3)→∀P:Prop.P
→(pr3 c t0 t3
→(∀u2:T
.pr3 c (THead (Flat Appl) x x0) u2
→((iso (THead (Flat Appl) x x0) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) t3 u2))
→sn3 c (THead (Flat Appl) t3 (THead (Flat Appl) x x0))))
case refl_equal : ⇒
the thesis becomes the hypothesis H6
∀t3:T
.(eq T t0 t3)→∀P:Prop.P
→(pr3 c t0 t3
→(∀u2:T
.pr3 c (THead (Flat Appl) x x0) u2
→((iso (THead (Flat Appl) x x0) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) t3 u2))
→sn3 c (THead (Flat Appl) t3 (THead (Flat Appl) x x0))))
end of H9
(H10)
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
→∀x1:T
.∀x2:T
.eq T t3 (THead (Flat Appl) x1 x2)
→∀v3:T
.sn3 c v3
→(∀u2:T.(pr3 c t3 u2)→((iso t3 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v3 u2))
→sn3 c (THead (Flat Appl) v3 t3)))
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
→∀x1:T
.∀x2:T
.eq T t3 (THead (Flat Appl) x1 x2)
→∀v3:T
.sn3 c v3
→(∀u2:T.(pr3 c t3 u2)→((iso t3 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v3 u2))
→sn3 c (THead (Flat Appl) v3 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)→(sn3 c t3)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
∀t3:T
.(eq T (THead (Flat Appl) x x0) t3)→∀P:Prop.P
→(pr3 c (THead (Flat Appl) x x0) t3)→(sn3 c t3)
end of H11
assume t3: T
suppose H12:
eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t3
→∀P:Prop.P
suppose H13: pr2 c (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t3
(H14)
by (pr2_gen_appl . . . . H13)
or3
ex3_2
T
T
λu2:T.λt2:T.eq T t3 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr2 c t0 u2
λ:T.λt2:T.pr2 c (THead (Flat Appl) x x0) t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T (THead (Flat Appl) x 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 t0 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 Appl) x 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 t0 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 H14
we proceed by induction on H14 to prove sn3 c t3
case or3_intro0 : H15:ex3_2 T T λu2:T.λt4:T.eq T t3 (THead (Flat Appl) u2 t4) λu2:T.λ:T.pr2 c t0 u2 λ:T.λt4:T.pr2 c (THead (Flat Appl) x x0) t4 ⇒
the thesis becomes sn3 c t3
we proceed by induction on H15 to prove sn3 c t3
case ex3_2_intro : x1:T x2:T H16:eq T t3 (THead (Flat Appl) x1 x2) H17:pr2 c t0 x1 H18:pr2 c (THead (Flat Appl) x x0) x2 ⇒
the thesis becomes sn3 c t3
(H19)
we proceed by induction on H16 to prove
(eq
T
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
THead (Flat Appl) x1 x2)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H12
(eq
T
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
THead (Flat Appl) x1 x2)
→∀P:Prop.P
end of H19
(H20)
by (pr2_gen_appl . . . . H18)
or3
ex3_2 T T λu2:T.λt2:T.eq T x2 (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr2 c x u2 λ:T.λt2:T.pr2 c x0 t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T x0 (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T x2 (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 x0 (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T
.λy2:T.eq T x2 (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 H20
we proceed by induction on H20 to prove sn3 c (THead (Flat Appl) x1 x2)
case or3_intro0 : H21:ex3_2 T T λu2:T.λt4:T.eq T x2 (THead (Flat Appl) u2 t4) λu2:T.λ:T.pr2 c x u2 λ:T.λt4:T.pr2 c x0 t4 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 x2)
we proceed by induction on H21 to prove sn3 c (THead (Flat Appl) x1 x2)
case ex3_2_intro : x3:T x4:T H22:eq T x2 (THead (Flat Appl) x3 x4) H23:pr2 c x x3 H24:pr2 c x0 x4 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 x2)
(H25)
we proceed by induction on H22 to prove
(eq
T
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H19
(eq
T
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))
→∀P:Prop.P
end of H25
(H_x)
by (term_dec . .)
or
eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4)
eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4)
→∀P:Prop.P
end of H_x
(H26) consider H_x
we proceed by induction on H26 to prove sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))
case or_introl : H27:eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4) ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))
(H28)
by (f_equal . . . . . H27)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) x x0 OF
TSort ⇒x
| TLRef ⇒x
| THead t ⇒t
<λ:T.T>
CASE THead (Flat Appl) x3 x4 OF
TSort ⇒x
| TLRef ⇒x
| THead t ⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t ⇒t
THead (Flat Appl) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t ⇒t
THead (Flat Appl) x3 x4
end of H28
(h1)
(H29)
by (f_equal . . . . . H27)
we proved
eq
T
<λ:T.T> CASE THead (Flat Appl) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t⇒t
<λ:T.T> CASE THead (Flat Appl) x3 x4 OF TSort ⇒x0 | TLRef ⇒x0 | THead t⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t⇒t
THead (Flat Appl) x x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t⇒t
THead (Flat Appl) x3 x4
end of H29
suppose H30: eq T x x3
(H31)
consider H29
we proved
eq
T
<λ:T.T> CASE THead (Flat Appl) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t⇒t
<λ:T.T> CASE THead (Flat Appl) x3 x4 OF TSort ⇒x0 | TLRef ⇒x0 | THead t⇒t
that is equivalent to eq T x0 x4
by (eq_ind_r . . . H25 . previous)
(eq
T
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
THead (Flat Appl) x1 (THead (Flat Appl) x3 x0))
→∀P:Prop.P
end of H31
consider H29
we proved
eq
T
<λ:T.T> CASE THead (Flat Appl) x x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t⇒t
<λ:T.T> CASE THead (Flat Appl) x3 x4 OF TSort ⇒x0 | TLRef ⇒x0 | THead t⇒t
that is equivalent to eq T x0 x4
we proceed by induction on the previous result to prove sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x0))
(H33)
by (eq_ind_r . . . H31 . H30)
(eq
T
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
THead (Flat Appl) x1 (THead (Flat Appl) x x0))
→∀P:Prop.P
end of H33
we proceed by induction on H30 to prove sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x0))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x x0))
(H_x0)
by (term_dec . .)
or (eq T t0 x1) (eq T t0 x1)→∀P:Prop.P
end of H_x0
(H35) consider H_x0
we proceed by induction on H35 to prove sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x x0))
case or_introl : H36:eq T t0 x1 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x x0))
(H37)
by (eq_ind_r . . . H33 . H36)
(eq
T
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
THead (Flat Appl) t0 (THead (Flat Appl) x x0))
→∀P:Prop.P
end of H37
we proceed by induction on H36 to prove sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x x0))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) t0 (THead (Flat Appl) x x0))
by (refl_equal . .)
we proved
eq
T
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
by (H37 previous .)
sn3 c (THead (Flat Appl) t0 (THead (Flat Appl) x x0))
sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x x0))
case or_intror : H36:(eq T t0 x1)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x x0))
(h1) by (pr3_pr2 . . . H17) we proved pr3 c t0 x1
(h2)
assume u2: T
suppose H37: pr3 c (THead (Flat Appl) x x0) u2
suppose H38: (iso (THead (Flat Appl) x x0) u2)→∀P:Prop.P
(h1)
by (H8 . H37 H38)
sn3 c (THead (Flat Appl) t0 u2)
end of h1
(h2)
by (pr2_head_1 . . . H17 . .)
we proved pr2 c (THead (Flat Appl) t0 u2) (THead (Flat Appl) x1 u2)
by (pr3_pr2 . . . previous)
pr3 c (THead (Flat Appl) t0 u2) (THead (Flat Appl) x1 u2)
end of h2
by (sn3_pr3_trans . . h1 . h2)
we proved sn3 c (THead (Flat Appl) x1 u2)
∀u2:T
.pr3 c (THead (Flat Appl) x x0) u2
→((iso (THead (Flat Appl) x x0) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) x1 u2))
end of h2
by (H9 . H36 h1 h2)
sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x x0))
sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x x0))
sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x0))
we proved sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))
(eq T x x3)→(sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4)))
end of h1
(h2)
consider H28
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) x x0 OF
TSort ⇒x
| TLRef ⇒x
| THead t ⇒t
<λ:T.T>
CASE THead (Flat Appl) x3 x4 OF
TSort ⇒x
| TLRef ⇒x
| THead t ⇒t
eq T x x3
end of h2
by (h1 h2)
sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))
case or_intror : H27:(eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4))→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))
(h1)
(h1) by (pr3_pr2 . . . H23) we proved pr3 c x x3
(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) x3 x4)
end of h1
(h2)
by (refl_equal . .)
eq T (THead (Flat Appl) x3 x4) (THead (Flat Appl) x3 x4)
end of h2
(h3)
(h1) by (sn3_sing . . H5) we proved sn3 c t0
(h2) by (pr3_pr2 . . . H17) we proved pr3 c t0 x1
by (sn3_pr3_trans . . h1 . h2)
sn3 c x1
end of h3
(h4)
assume u2: T
suppose H28: pr3 c (THead (Flat Appl) x3 x4) u2
suppose H29: (iso (THead (Flat Appl) x3 x4) u2)→∀P:Prop.P
(h1)
(h1)
(h1)
by (pr2_thin_dx . . . H24 . .)
pr2 c (THead (Flat Appl) x x0) (THead (Flat Appl) x x4)
end of h1
(h2)
by (pr2_head_1 . . . H23 . .)
we proved pr2 c (THead (Flat Appl) x x4) (THead (Flat Appl) x3 x4)
by (pr3_sing . . . previous . H28)
pr3 c (THead (Flat Appl) x x4) u2
end of h2
by (pr3_sing . . . h1 . h2)
pr3 c (THead (Flat Appl) x x0) u2
end of h1
(h2)
suppose H30: iso (THead (Flat Appl) x x0) u2
assume P: Prop
by (iso_head . . . . .)
we proved iso (THead (Flat Appl) x3 x4) (THead (Flat Appl) x x0)
by (iso_trans . . previous . H30)
we proved iso (THead (Flat Appl) x3 x4) u2
by (H29 previous .)
we proved P
(iso (THead (Flat Appl) x x0) u2)→∀P:Prop.P
end of h2
by (H8 . h1 h2)
sn3 c (THead (Flat Appl) t0 u2)
end of h1
(h2)
by (pr2_head_1 . . . H17 . .)
we proved pr2 c (THead (Flat Appl) t0 u2) (THead (Flat Appl) x1 u2)
by (pr3_pr2 . . . previous)
pr3 c (THead (Flat Appl) t0 u2) (THead (Flat Appl) x1 u2)
end of h2
by (sn3_pr3_trans . . h1 . h2)
we proved sn3 c (THead (Flat Appl) x1 u2)
∀u2:T
.pr3 c (THead (Flat Appl) x3 x4) u2
→((iso (THead (Flat Appl) x3 x4) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) x1 u2))
end of h4
by (H10 . H27 h1 . . h2 . h3 h4)
sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))
we proved sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))
by (eq_ind_r . . . previous . H22)
sn3 c (THead (Flat Appl) x1 x2)
sn3 c (THead (Flat Appl) x1 x2)
case or3_intro1 : H21:ex4_4 T T T T λy1:T.λz1:T.λ:T.λ:T.eq T x0 (THead (Bind Abst) y1 z1) λ:T.λ:T.λu2:T.λt4:T.eq T x2 (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 (THead (Flat Appl) x1 x2)
we proceed by induction on H21 to prove sn3 c (THead (Flat Appl) x1 x2)
case ex4_4_intro : x3:T x4:T x5:T x6:T H22:eq T x0 (THead (Bind Abst) x3 x4) H23:eq T x2 (THead (Bind Abbr) x5 x6) H24:pr2 c x x5 H25:∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x4 x6) ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 x2)
(H26)
we proceed by induction on H23 to prove
(eq
T
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
THead (Flat Appl) x1 (THead (Bind Abbr) x5 x6))
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H19
(eq
T
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
THead (Flat Appl) x1 (THead (Bind Abbr) x5 x6))
→∀P:Prop.P
end of H26
(H30)
we proceed by induction on H22 to prove
∀u2:T
.pr3 c (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) u2
→(iso (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) u2
→∀P:Prop.P
→sn3 c (THead (Flat Appl) t0 u2))
case refl_equal : ⇒
the thesis becomes the hypothesis H8
∀u2:T
.pr3 c (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) u2
→(iso (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) u2
→∀P:Prop.P
→sn3 c (THead (Flat Appl) t0 u2))
end of H30
(h1)
(h1)
(h1)
(h1) by (pr0_refl .) we proved pr0 x x
(h2) by (pr0_refl .) we proved pr0 x4 x4
by (pr0_beta . . . h1 . . h2)
we proved
pr0
THead (Flat Appl) x (THead (Bind Abst) x3 x4)
THead (Bind Abbr) x x4
by (pr2_free . . . previous)
pr2
c
THead (Flat Appl) x (THead (Bind Abst) x3 x4)
THead (Bind Abbr) x x4
end of h1
(h2)
(h1) by (pr3_pr2 . . . H24) we proved pr3 c x x5
(h2)
by (H25 . .)
we proved pr2 (CHead c (Bind Abbr) x5) x4 x6
by (pr3_pr2 . . . previous)
pr3 (CHead c (Bind Abbr) x5) x4 x6
end of h2
by (pr3_head_12 . . . h1 . . . h2)
pr3 c (THead (Bind Abbr) x x4) (THead (Bind Abbr) x5 x6)
end of h2
by (pr3_sing . . . h1 . h2)
pr3
c
THead (Flat Appl) x (THead (Bind Abst) x3 x4)
THead (Bind Abbr) x5 x6
end of h1
(h2)
suppose H32:
iso
THead (Flat Appl) x (THead (Bind Abst) x3 x4)
THead (Bind Abbr) x5 x6
assume P: Prop
(H33)
by cases on H32 we prove
(eq
T
THead (Flat Appl) x (THead (Bind Abst) x3 x4)
THead (Flat Appl) x (THead (Bind Abst) x3 x4))
→(eq T (THead (Bind Abbr) x5 x6) (THead (Bind Abbr) x5 x6))→P
case iso_sort n1:nat n2:nat ⇒
the thesis becomes
∀H33:eq T (TSort n1) (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
.∀H34:(eq T (TSort n2) (THead (Bind Abbr) x5 x6)).P
suppose H33: eq T (TSort n1) (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
suppose H34: eq T (TSort n2) (THead (Bind Abbr) x5 x6)
(H35)
we proceed by induction on H33 to prove
<λ:T.Prop>
CASE THead (Flat Appl) x (THead (Bind Abst) x3 x4) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n1 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n1 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE THead (Flat Appl) x (THead (Bind Abst) x3 x4) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H35
consider H35
we proved
<λ:T.Prop>
CASE THead (Flat Appl) x (THead (Bind Abst) x3 x4) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove (eq T (TSort n2) (THead (Bind Abbr) x5 x6))→P
we proved (eq T (TSort n2) (THead (Bind Abbr) x5 x6))→P
by (previous H34)
we proved P
∀H33:eq T (TSort n1) (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
.∀H34:(eq T (TSort n2) (THead (Bind Abbr) x5 x6)).P
case iso_lref i1:nat i2:nat ⇒
the thesis becomes
∀H33:eq T (TLRef i1) (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
.∀H34:(eq T (TLRef i2) (THead (Bind Abbr) x5 x6)).P
suppose H33: eq T (TLRef i1) (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
suppose H34: eq T (TLRef i2) (THead (Bind Abbr) x5 x6)
(H35)
we proceed by induction on H33 to prove
<λ:T.Prop>
CASE THead (Flat Appl) x (THead (Bind Abst) x3 x4) OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Flat Appl) x (THead (Bind Abst) x3 x4) OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H35
consider H35
we proved
<λ:T.Prop>
CASE THead (Flat Appl) x (THead (Bind Abst) x3 x4) OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove (eq T (TLRef i2) (THead (Bind Abbr) x5 x6))→P
we proved (eq T (TLRef i2) (THead (Bind Abbr) x5 x6))→P
by (previous H34)
we proved P
∀H33:eq T (TLRef i1) (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
.∀H34:(eq T (TLRef i2) (THead (Bind Abbr) x5 x6)).P
case iso_head v4:T v5:T t4:T t5:T k:K ⇒
the thesis becomes
∀H33:eq T (THead k v4 t4) (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
.∀H34:(eq T (THead k v5 t5) (THead (Bind Abbr) x5 x6)).P
suppose H33: eq T (THead k v4 t4) (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
suppose H34: eq T (THead k v5 t5) (THead (Bind Abbr) x5 x6)
(H35)
by (f_equal . . . . . H33)
we proved
eq
T
<λ:T.T> CASE THead k v4 t4 OF TSort ⇒t4 | TLRef ⇒t4 | THead t⇒t
<λ:T.T>
CASE THead (Flat Appl) x (THead (Bind Abst) x3 x4) OF
TSort ⇒t4
| TLRef ⇒t4
| THead t⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t4 | TLRef ⇒t4 | THead t⇒t (THead k v4 t4)
λe:T.<λ:T.T> CASE e OF TSort ⇒t4 | TLRef ⇒t4 | THead t⇒t
THead (Flat Appl) x (THead (Bind Abst) x3 x4)
end of H35
(h1)
(H36)
by (f_equal . . . . . H33)
we proved
eq
T
<λ:T.T> CASE THead k v4 t4 OF TSort ⇒v4 | TLRef ⇒v4 | THead t ⇒t
<λ:T.T>
CASE THead (Flat Appl) x (THead (Bind Abst) x3 x4) OF
TSort ⇒v4
| TLRef ⇒v4
| THead t ⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒v4 | TLRef ⇒v4 | THead t ⇒t (THead k v4 t4)
λe:T.<λ:T.T> CASE e OF TSort ⇒v4 | TLRef ⇒v4 | THead t ⇒t
THead (Flat Appl) x (THead (Bind Abst) x3 x4)
end of H36
(h1)
(H37)
by (f_equal . . . . . H33)
we proved
eq
K
<λ:T.K> CASE THead k v4 t4 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K>
CASE THead (Flat Appl) x (THead (Bind Abst) x3 x4) OF
TSort ⇒k
| TLRef ⇒k
| THead k0 ⇒k0
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0 (THead k v4 t4)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
THead (Flat Appl) x (THead (Bind Abst) x3 x4)
end of H37
consider H37
we proved
eq
K
<λ:T.K> CASE THead k v4 t4 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K>
CASE THead (Flat Appl) x (THead (Bind Abst) x3 x4) OF
TSort ⇒k
| TLRef ⇒k
| THead k0 ⇒k0
that is equivalent to eq K k (Flat Appl)
by (sym_eq . . . previous)
we proved eq K (Flat Appl) k
we proceed by induction on the previous result to prove
eq T v4 x
→(eq T t4 (THead (Bind Abst) x3 x4)
→(eq T (THead k v5 t5) (THead (Bind Abbr) x5 x6))→P)
case refl_equal : ⇒
the thesis becomes
eq T v4 x
→(eq T t4 (THead (Bind Abst) x3 x4)
→(eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6))→P)
suppose H38: eq T v4 x
by (sym_eq . . . H38)
we proved eq T x v4
we proceed by induction on the previous result to prove
eq T t4 (THead (Bind Abst) x3 x4)
→(eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6))→P
case refl_equal : ⇒
the thesis becomes
eq T t4 (THead (Bind Abst) x3 x4)
→(eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6))→P
suppose H39: eq T t4 (THead (Bind Abst) x3 x4)
by (sym_eq . . . H39)
we proved eq T (THead (Bind Abst) x3 x4) t4
we proceed by induction on the previous result to prove (eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6))→P
case refl_equal : ⇒
the thesis becomes (eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6))→P
suppose H40: eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6)
(H41)
we proceed by induction on H40 to prove
<λ:T.Prop>
CASE THead (Bind Abbr) x5 x6 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) v5 t5 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) v5 t5 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind Abbr) x5 x6 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
end of H41
consider H41
we proved
<λ:T.Prop>
CASE THead (Bind Abbr) x5 x6 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) v5 t5) (THead (Bind Abbr) x5 x6))→P
we proved (eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6))→P
eq T t4 (THead (Bind Abst) x3 x4)
→(eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6))→P
we proved
eq T t4 (THead (Bind Abst) x3 x4)
→(eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6))→P
eq T v4 x
→(eq T t4 (THead (Bind Abst) x3 x4)
→(eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6))→P)
eq T v4 x
→(eq T t4 (THead (Bind Abst) x3 x4)
→(eq T (THead k v5 t5) (THead (Bind Abbr) x5 x6))→P)
end of h1
(h2)
consider H36
we proved
eq
T
<λ:T.T> CASE THead k v4 t4 OF TSort ⇒v4 | TLRef ⇒v4 | THead t ⇒t
<λ:T.T>
CASE THead (Flat Appl) x (THead (Bind Abst) x3 x4) OF
TSort ⇒v4
| TLRef ⇒v4
| THead t ⇒t
eq T v4 x
end of h2
by (h1 h2)
eq T t4 (THead (Bind Abst) x3 x4)
→(eq T (THead k v5 t5) (THead (Bind Abbr) x5 x6))→P
end of h1
(h2)
consider H35
we proved
eq
T
<λ:T.T> CASE THead k v4 t4 OF TSort ⇒t4 | TLRef ⇒t4 | THead t⇒t
<λ:T.T>
CASE THead (Flat Appl) x (THead (Bind Abst) x3 x4) OF
TSort ⇒t4
| TLRef ⇒t4
| THead t⇒t
eq T t4 (THead (Bind Abst) x3 x4)
end of h2
by (h1 h2)
we proved (eq T (THead k v5 t5) (THead (Bind Abbr) x5 x6))→P
by (previous H34)
we proved P
∀H33:eq T (THead k v4 t4) (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
.∀H34:(eq T (THead k v5 t5) (THead (Bind Abbr) x5 x6)).P
(eq
T
THead (Flat Appl) x (THead (Bind Abst) x3 x4)
THead (Flat Appl) x (THead (Bind Abst) x3 x4))
→(eq T (THead (Bind Abbr) x5 x6) (THead (Bind Abbr) x5 x6))→P
end of H33
(h1)
by (refl_equal . .)
eq
T
THead (Flat Appl) x (THead (Bind Abst) x3 x4)
THead (Flat Appl) x (THead (Bind Abst) x3 x4)
end of h1
(h2)
by (refl_equal . .)
eq T (THead (Bind Abbr) x5 x6) (THead (Bind Abbr) x5 x6)
end of h2
by (H33 h1 h2)
we proved P
(iso
THead (Flat Appl) x (THead (Bind Abst) x3 x4)
THead (Bind Abbr) x5 x6)
→∀P:Prop.P
end of h2
by (H30 . h1 h2)
sn3 c (THead (Flat Appl) t0 (THead (Bind Abbr) x5 x6))
end of h1
(h2)
by (pr2_head_1 . . . H17 . .)
we proved
pr2
c
THead (Flat Appl) t0 (THead (Bind Abbr) x5 x6)
THead (Flat Appl) x1 (THead (Bind Abbr) x5 x6)
by (pr3_pr2 . . . previous)
pr3
c
THead (Flat Appl) t0 (THead (Bind Abbr) x5 x6)
THead (Flat Appl) x1 (THead (Bind Abbr) x5 x6)
end of h2
by (sn3_pr3_trans . . h1 . h2)
we proved sn3 c (THead (Flat Appl) x1 (THead (Bind Abbr) x5 x6))
by (eq_ind_r . . . previous . H23)
sn3 c (THead (Flat Appl) x1 x2)
sn3 c (THead (Flat Appl) x1 x2)
case or3_intro2 : H21: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 x0 (THead (Bind b) y1 z1) λb:B.λ:T.λ:T.λz2:T.λu2:T.λy2:T.eq T x2 (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 (THead (Flat Appl) x1 x2)
we proceed by induction on H21 to prove sn3 c (THead (Flat Appl) x1 x2)
case ex6_6_intro : x3:B x4:T x5:T x6:T x7:T x8:T H22:not (eq B x3 Abst) H23:eq T x0 (THead (Bind x3) x4 x5) H24:eq T x2 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)) H25:pr2 c x x7 H26:pr2 c x4 x8 H27:pr2 (CHead c (Bind x3) x8) x5 x6 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 x2)
(H28)
we proceed by induction on H24 to prove
(eq
T
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
THead
Flat Appl
x1
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H19
(eq
T
THead (Flat Appl) t0 (THead (Flat Appl) x x0)
THead
Flat Appl
x1
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→∀P:Prop.P
end of H28
(H32)
we proceed by induction on H23 to prove
∀u2:T
.pr3 c (THead (Flat Appl) x (THead (Bind x3) x4 x5)) u2
→((iso (THead (Flat Appl) x (THead (Bind x3) x4 x5)) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) t0 u2))
case refl_equal : ⇒
the thesis becomes the hypothesis H8
∀u2:T
.pr3 c (THead (Flat Appl) x (THead (Bind x3) x4 x5)) u2
→((iso (THead (Flat Appl) x (THead (Bind x3) x4 x5)) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) t0 u2))
end of H32
(h1)
(h1)
(h1)
(h1) by (pr0_refl .) we proved pr0 x x
(h2) by (pr0_refl .) we proved pr0 x4 x4
(h3) by (pr0_refl .) we proved pr0 x5 x5
by (pr0_upsilon . H22 . . h1 . . h2 . . h3)
we proved
pr0
THead (Flat Appl) x (THead (Bind x3) x4 x5)
THead (Bind x3) x4 (THead (Flat Appl) (lift (S O) O x) x5)
by (pr2_free . . . previous)
pr2
c
THead (Flat Appl) x (THead (Bind x3) x4 x5)
THead (Bind x3) x4 (THead (Flat Appl) (lift (S O) O x) x5)
end of h1
(h2)
(h1) by (pr3_pr2 . . . H26) we proved pr3 c x4 x8
(h2)
(h1)
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind x3) O) O c c
by (drop_drop . . . . previous .)
drop (S O) O (CHead c (Bind x3) x8) c
end of h1
(h2) by (pr3_pr2 . . . H25) we proved pr3 c x x7
by (pr3_lift . . . . h1 . . h2)
pr3 (CHead c (Bind x3) x8) (lift (S O) O x) (lift (S O) O x7)
end of h1
(h2)
by (pr2_cflat . . . H27 . .)
we proved pr2 (CHead (CHead c (Bind x3) x8) (Flat Appl) (lift (S O) O x7)) x5 x6
by (pr3_pr2 . . . previous)
pr3 (CHead (CHead c (Bind x3) x8) (Flat Appl) (lift (S O) O x7)) x5 x6
end of h2
by (pr3_head_12 . . . h1 . . . h2)
pr3
CHead c (Bind x3) x8
THead (Flat Appl) (lift (S O) O x) x5
THead (Flat Appl) (lift (S O) O x7) x6
end of h2
by (pr3_head_12 . . . h1 . . . h2)
pr3
c
THead (Bind x3) x4 (THead (Flat Appl) (lift (S O) O x) x5)
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
end of h2
by (pr3_sing . . . h1 . h2)
pr3
c
THead (Flat Appl) x (THead (Bind x3) x4 x5)
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
end of h1
(h2)
suppose H34:
iso
THead (Flat Appl) x (THead (Bind x3) x4 x5)
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
assume P: Prop
(H35)
by cases on H34 we prove
(eq
T
THead (Flat Appl) x (THead (Bind x3) x4 x5)
THead (Flat Appl) x (THead (Bind x3) x4 x5))
→((eq
T
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P)
case iso_sort n1:nat n2:nat ⇒
the thesis becomes
∀H35:eq T (TSort n1) (THead (Flat Appl) x (THead (Bind x3) x4 x5))
.∀H36:eq
T
TSort n2
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
.P
suppose H35: eq T (TSort n1) (THead (Flat Appl) x (THead (Bind x3) x4 x5))
suppose H36:
eq
T
TSort n2
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
(H37)
we proceed by induction on H35 to prove
<λ:T.Prop>
CASE THead (Flat Appl) x (THead (Bind x3) x4 x5) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n1 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n1 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE THead (Flat Appl) x (THead (Bind x3) x4 x5) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H37
consider H37
we proved
<λ:T.Prop>
CASE THead (Flat Appl) x (THead (Bind x3) x4 x5) OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
(eq
T
TSort n2
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P
we proved
(eq
T
TSort n2
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P
by (previous H36)
we proved P
∀H35:eq T (TSort n1) (THead (Flat Appl) x (THead (Bind x3) x4 x5))
.∀H36:eq
T
TSort n2
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
.P
case iso_lref i1:nat i2:nat ⇒
the thesis becomes
∀H35:eq T (TLRef i1) (THead (Flat Appl) x (THead (Bind x3) x4 x5))
.∀H36:eq
T
TLRef i2
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
.P
suppose H35: eq T (TLRef i1) (THead (Flat Appl) x (THead (Bind x3) x4 x5))
suppose H36:
eq
T
TLRef i2
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
(H37)
we proceed by induction on H35 to prove
<λ:T.Prop>
CASE THead (Flat Appl) x (THead (Bind x3) x4 x5) OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Flat Appl) x (THead (Bind x3) x4 x5) OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H37
consider H37
we proved
<λ:T.Prop>
CASE THead (Flat Appl) x (THead (Bind x3) x4 x5) OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
(eq
T
TLRef i2
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P
we proved
(eq
T
TLRef i2
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P
by (previous H36)
we proved P
∀H35:eq T (TLRef i1) (THead (Flat Appl) x (THead (Bind x3) x4 x5))
.∀H36:eq
T
TLRef i2
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
.P
case iso_head v4:T v5:T t4:T t5:T k:K ⇒
the thesis becomes
∀H35:eq T (THead k v4 t4) (THead (Flat Appl) x (THead (Bind x3) x4 x5))
.∀H36:eq
T
THead k v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
.P
suppose H35: eq T (THead k v4 t4) (THead (Flat Appl) x (THead (Bind x3) x4 x5))
suppose H36:
eq
T
THead k v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
(H37)
by (f_equal . . . . . H35)
we proved
eq
T
<λ:T.T> CASE THead k v4 t4 OF TSort ⇒t4 | TLRef ⇒t4 | THead t⇒t
<λ:T.T>
CASE THead (Flat Appl) x (THead (Bind x3) x4 x5) OF
TSort ⇒t4
| TLRef ⇒t4
| THead t⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t4 | TLRef ⇒t4 | THead t⇒t (THead k v4 t4)
λe:T.<λ:T.T> CASE e OF TSort ⇒t4 | TLRef ⇒t4 | THead t⇒t
THead (Flat Appl) x (THead (Bind x3) x4 x5)
end of H37
(h1)
(H38)
by (f_equal . . . . . H35)
we proved
eq
T
<λ:T.T> CASE THead k v4 t4 OF TSort ⇒v4 | TLRef ⇒v4 | THead t ⇒t
<λ:T.T>
CASE THead (Flat Appl) x (THead (Bind x3) x4 x5) OF
TSort ⇒v4
| TLRef ⇒v4
| THead t ⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒v4 | TLRef ⇒v4 | THead t ⇒t (THead k v4 t4)
λe:T.<λ:T.T> CASE e OF TSort ⇒v4 | TLRef ⇒v4 | THead t ⇒t
THead (Flat Appl) x (THead (Bind x3) x4 x5)
end of H38
(h1)
(H39)
by (f_equal . . . . . H35)
we proved
eq
K
<λ:T.K> CASE THead k v4 t4 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K>
CASE THead (Flat Appl) x (THead (Bind x3) x4 x5) OF
TSort ⇒k
| TLRef ⇒k
| THead k0 ⇒k0
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0 (THead k v4 t4)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
THead (Flat Appl) x (THead (Bind x3) x4 x5)
end of H39
consider H39
we proved
eq
K
<λ:T.K> CASE THead k v4 t4 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K>
CASE THead (Flat Appl) x (THead (Bind x3) x4 x5) OF
TSort ⇒k
| TLRef ⇒k
| THead k0 ⇒k0
that is equivalent to eq K k (Flat Appl)
by (sym_eq . . . previous)
we proved eq K (Flat Appl) k
we proceed by induction on the previous result to prove
eq T v4 x
→(eq T t4 (THead (Bind x3) x4 x5)
→((eq
T
THead k v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P))
case refl_equal : ⇒
the thesis becomes
eq T v4 x
→(eq T t4 (THead (Bind x3) x4 x5)
→((eq
T
THead (Flat Appl) v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P))
suppose H40: eq T v4 x
by (sym_eq . . . H40)
we proved eq T x v4
we proceed by induction on the previous result to prove
eq T t4 (THead (Bind x3) x4 x5)
→((eq
T
THead (Flat Appl) v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P)
case refl_equal : ⇒
the thesis becomes
eq T t4 (THead (Bind x3) x4 x5)
→((eq
T
THead (Flat Appl) v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P)
suppose H41: eq T t4 (THead (Bind x3) x4 x5)
by (sym_eq . . . H41)
we proved eq T (THead (Bind x3) x4 x5) t4
we proceed by induction on the previous result to prove
(eq
T
THead (Flat Appl) v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P
case refl_equal : ⇒
the thesis becomes
(eq
T
THead (Flat Appl) v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P
suppose H42:
eq
T
THead (Flat Appl) v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
(H43)
we proceed by induction on H42 to prove
<λ:T.Prop>
CASE THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6) 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) v5 t5 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) v5 t5 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6) OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
end of H43
consider H43
we proved
<λ:T.Prop>
CASE THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6) 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) v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P
we proved
(eq
T
THead (Flat Appl) v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P
eq T t4 (THead (Bind x3) x4 x5)
→((eq
T
THead (Flat Appl) v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P)
we proved
eq T t4 (THead (Bind x3) x4 x5)
→((eq
T
THead (Flat Appl) v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P)
eq T v4 x
→(eq T t4 (THead (Bind x3) x4 x5)
→((eq
T
THead (Flat Appl) v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P))
eq T v4 x
→(eq T t4 (THead (Bind x3) x4 x5)
→((eq
T
THead k v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P))
end of h1
(h2)
consider H38
we proved
eq
T
<λ:T.T> CASE THead k v4 t4 OF TSort ⇒v4 | TLRef ⇒v4 | THead t ⇒t
<λ:T.T>
CASE THead (Flat Appl) x (THead (Bind x3) x4 x5) OF
TSort ⇒v4
| TLRef ⇒v4
| THead t ⇒t
eq T v4 x
end of h2
by (h1 h2)
eq T t4 (THead (Bind x3) x4 x5)
→((eq
T
THead k v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P)
end of h1
(h2)
consider H37
we proved
eq
T
<λ:T.T> CASE THead k v4 t4 OF TSort ⇒t4 | TLRef ⇒t4 | THead t⇒t
<λ:T.T>
CASE THead (Flat Appl) x (THead (Bind x3) x4 x5) OF
TSort ⇒t4
| TLRef ⇒t4
| THead t⇒t
eq T t4 (THead (Bind x3) x4 x5)
end of h2
by (h1 h2)
we proved
(eq
T
THead k v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P
by (previous H36)
we proved P
∀H35:eq T (THead k v4 t4) (THead (Flat Appl) x (THead (Bind x3) x4 x5))
.∀H36:eq
T
THead k v5 t5
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
.P
(eq
T
THead (Flat Appl) x (THead (Bind x3) x4 x5)
THead (Flat Appl) x (THead (Bind x3) x4 x5))
→((eq
T
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→P)
end of H35
(h1)
by (refl_equal . .)
eq
T
THead (Flat Appl) x (THead (Bind x3) x4 x5)
THead (Flat Appl) x (THead (Bind x3) x4 x5)
end of h1
(h2)
by (refl_equal . .)
eq
T
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
end of h2
by (H35 h1 h2)
we proved P
(iso
THead (Flat Appl) x (THead (Bind x3) x4 x5)
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
→∀P:Prop.P
end of h2
by (H32 . h1 h2)
sn3
c
THead
Flat Appl
t0
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
end of h1
(h2)
by (pr2_head_1 . . . H17 . .)
we proved
pr2
c
THead
Flat Appl
t0
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
THead
Flat Appl
x1
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
by (pr3_pr2 . . . previous)
pr3
c
THead
Flat Appl
t0
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
THead
Flat Appl
x1
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
end of h2
by (sn3_pr3_trans . . h1 . h2)
we proved
sn3
c
THead
Flat Appl
x1
THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)
by (eq_ind_r . . . previous . H24)
sn3 c (THead (Flat Appl) x1 x2)
sn3 c (THead (Flat Appl) x1 x2)
we proved sn3 c (THead (Flat Appl) x1 x2)
by (eq_ind_r . . . previous . H16)
sn3 c t3
sn3 c t3
case or3_intro1 : H15:ex4_4 T T T T λy1:T.λz1:T.λ:T.λ:T.eq T (THead (Flat Appl) x 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 t0 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 H15 to prove sn3 c t3
case ex4_4_intro : x1:T x2:T x3:T x4:T H16:eq T (THead (Flat Appl) x x0) (THead (Bind Abst) x1 x2) H17:eq T t3 (THead (Bind Abbr) x3 x4) :pr2 c t0 x3 :∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x2 x4) ⇒
the thesis becomes sn3 c t3
(H21)
we proceed by induction on H16 to prove
<λ:T.Prop>
CASE THead (Bind Abst) x1 x2 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 Appl) x x0 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 Appl) x x0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind Abst) x1 x2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
end of H21
consider H21
we proved
<λ:T.Prop>
CASE THead (Bind Abst) x1 x2 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) x3 x4)
we proved sn3 c (THead (Bind Abbr) x3 x4)
by (eq_ind_r . . . previous . H17)
sn3 c t3
sn3 c t3
case or3_intro2 : H15: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 Appl) x 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 t0 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 H15 to prove sn3 c t3
case ex6_6_intro : x1:B x2:T x3:T x4:T x5:T x6:T :not (eq B x1 Abst) H17:eq T (THead (Flat Appl) x x0) (THead (Bind x1) x2 x3) H18:eq T t3 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4)) :pr2 c t0 x5 :pr2 c x2 x6 :pr2 (CHead c (Bind x1) x6) x3 x4 ⇒
the thesis becomes sn3 c t3
(H23)
we proceed by induction on H17 to prove
<λ:T.Prop>
CASE THead (Bind x1) 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 Appl) x x0 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 Appl) x x0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind x1) x2 x3 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
end of H23
consider H23
we proved
<λ:T.Prop>
CASE THead (Bind x1) 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 x1) 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))
by (eq_ind_r . . . previous . H18)
sn3 c t3
sn3 c t3
we proved sn3 c t3
we proved
∀t3:T
.eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t3
→∀P:Prop.P
→(pr2 c (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t3)→(sn3 c t3)
by (sn3_pr2_intro . . previous)
we proved sn3 c (THead (Flat Appl) t0 (THead (Flat Appl) x x0))
by (eq_ind_r . . . previous . H3)
we proved sn3 c (THead (Flat Appl) t0 t2)
∀H7:∀u2:T.(pr3 c t2 u2)→((iso t2 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) t0 u2))
.sn3 c (THead (Flat Appl) t0 t2)
we proved
∀u2:T.(pr3 c t2 u2)→((iso t2 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 t2)
∀x:T
.∀x0:T
.∀H3:eq T t2 (THead (Flat Appl) x x0)
.∀v2:T
.∀H4:sn3 c v2
.∀u2:T.(pr3 c t2 u2)→((iso t2 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 t2)
we proved
∀x:T
.∀x0:T
.eq T y (THead (Flat Appl) x x0)
→∀v2:T
.sn3 c v2
→(∀u2:T
.pr3 c y u2
→((iso y u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 y))
by (unintro . . . previous)
we proved
∀x:T
.eq T y (THead (Flat Appl) v1 x)
→∀v2:T
.sn3 c v2
→(∀u2:T
.pr3 c y u2
→((iso y u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 y))
by (unintro . . . previous)
we proved
eq T y (THead (Flat Appl) v1 t1)
→∀v2:T
.sn3 c v2
→(∀u2:T
.pr3 c y u2
→((iso y u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 y))
we proved
∀y:T
.sn3 c y
→(eq T y (THead (Flat Appl) v1 t1)
→∀v2:T
.sn3 c v2
→(∀u2:T
.pr3 c y u2
→((iso y u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 y)))
by (insert_eq . . . . previous H)
we proved
∀v2:T
.sn3 c v2
→(∀u2:T
.pr3 c (THead (Flat Appl) v1 t1) u2
→((iso (THead (Flat Appl) v1 t1) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 (THead (Flat Appl) v1 t1)))
we proved
∀c:C
.sn3 c (THead (Flat Appl) v1 t1)
→∀v2:T
.sn3 c v2
→(∀u2:T
.pr3 c (THead (Flat Appl) v1 t1) u2
→((iso (THead (Flat Appl) v1 t1) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 (THead (Flat Appl) v1 t1)))
that is equivalent to
let u1 := THead (Flat Appl) v1 t1
in ∀c:C
.sn3 c u1
→∀v2:T
.sn3 c v2
→(∀u2:T.(pr3 c u1 u2)→((iso u1 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 u1))
we proved
∀v1:T
.∀t1:T
.let u1 := THead (Flat Appl) v1 t1
in ∀c:C
.sn3 c u1
→∀v2:T
.sn3 c v2
→(∀u2:T.(pr3 c u1 u2)→((iso u1 u2)→∀P:Prop.P)→(sn3 c (THead (Flat Appl) v2 u2))
→sn3 c (THead (Flat Appl) v2 u1))