DEFINITION pr3_iso_beta()
TYPE =
∀v:T
.∀w:T
.∀t:T
.let u1 := THead (Flat Appl) v (THead (Bind Abst) w t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THead (Bind Abbr) v t) u2)
BODY =
assume v: T
assume w: T
assume t: T
we must prove
let u1 := THead (Flat Appl) v (THead (Bind Abst) w t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THead (Bind Abbr) v t) u2)
or equivalently
∀c:C
.∀u2:T
.pr3 c (THead (Flat Appl) v (THead (Bind Abst) w t)) u2
→(iso (THead (Flat Appl) v (THead (Bind Abst) w t)) u2
→∀P:Prop.P
→pr3 c (THead (Bind Abbr) v t) u2)
assume c: C
assume u2: T
suppose H: pr3 c (THead (Flat Appl) v (THead (Bind Abst) w t)) u2
suppose H0:
iso (THead (Flat Appl) v (THead (Bind Abst) w t)) u2
→∀P:Prop.P
(H1)
by (pr3_gen_appl . . . . H)
or3
ex3_2
T
T
λu2:T.λt2:T.eq T u2 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr3 c v u2
λ:T.λt2:T.pr3 c (THead (Bind Abst) w t) t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) u2
λ:T.λ:T.λu2:T.λ:T.pr3 c v u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c (THead (Bind Abst) w t) (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (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.pr3 c (THead (Bind Abst) w t) (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) u2
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c v u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
end of H1
we proceed by induction on H1 to prove pr3 c (THead (Bind Abbr) v t) u2
case or3_intro0 : H2:ex3_2 T T λu3:T.λt2:T.eq T u2 (THead (Flat Appl) u3 t2) λu3:T.λ:T.pr3 c v u3 λ:T.λt2:T.pr3 c (THead (Bind Abst) w t) t2 ⇒
the thesis becomes pr3 c (THead (Bind Abbr) v t) u2
we proceed by induction on H2 to prove pr3 c (THead (Bind Abbr) v t) u2
case ex3_2_intro : x0:T x1:T H3:eq T u2 (THead (Flat Appl) x0 x1) :pr3 c v x0 :pr3 c (THead (Bind Abst) w t) x1 ⇒
the thesis becomes pr3 c (THead (Bind Abbr) v t) u2
(H6)
we proceed by induction on H3 to prove
(iso
THead (Flat Appl) v (THead (Bind Abst) w t)
THead (Flat Appl) x0 x1)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H0
(iso
THead (Flat Appl) v (THead (Bind Abst) w t)
THead (Flat Appl) x0 x1)
→∀P:Prop.P
end of H6
by (iso_head . . . . .)
we proved
iso
THead (Flat Appl) v (THead (Bind Abst) w t)
THead (Flat Appl) x0 x1
by (H6 previous .)
we proved pr3 c (THead (Bind Abbr) v t) (THead (Flat Appl) x0 x1)
by (eq_ind_r . . . previous . H3)
pr3 c (THead (Bind Abbr) v t) u2
pr3 c (THead (Bind Abbr) v t) u2
case or3_intro1 : H2:ex4_4 T T T T λ:T.λ:T.λu3:T.λt2:T.pr3 c (THead (Bind Abbr) u3 t2) u2 λ:T.λ:T.λu3:T.λ:T.pr3 c v u3 λy1:T.λz1:T.λ:T.λ:T.pr3 c (THead (Bind Abst) w t) (THead (Bind Abst) y1 z1) λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2) ⇒
the thesis becomes pr3 c (THead (Bind Abbr) v t) u2
we proceed by induction on H2 to prove pr3 c (THead (Bind Abbr) v t) u2
case ex4_4_intro : x0:T x1:T x2:T x3:T H3:pr3 c (THead (Bind Abbr) x2 x3) u2 H4:pr3 c v x2 H5:pr3 c (THead (Bind Abst) w t) (THead (Bind Abst) x0 x1) H6:∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 x3) ⇒
the thesis becomes pr3 c (THead (Bind Abbr) v t) u2
(H7)
by (pr3_gen_abst . . . . H5)
ex3_2
T
T
λu2:T.λt2:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c w u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t t2)
end of H7
we proceed by induction on H7 to prove pr3 c (THead (Bind Abbr) v t) u2
case ex3_2_intro : x4:T x5:T H8:eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) x4 x5) H9:pr3 c w x4 H10:∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t x5) ⇒
the thesis becomes pr3 c (THead (Bind Abbr) v t) u2
(H11)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) x0 x1 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abst) x4 x5 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) x0 x1
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0 ⇒t0
THead (Bind Abst) x4 x5
end of H11
(h1)
(H12)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) x0 x1 OF TSort ⇒x1 | TLRef ⇒x1 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abst) x4 x5 OF TSort ⇒x1 | TLRef ⇒x1 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x1 | TLRef ⇒x1 | THead t0⇒t0
THead (Bind Abst) x0 x1
λe:T.<λ:T.T> CASE e OF TSort ⇒x1 | TLRef ⇒x1 | THead t0⇒t0
THead (Bind Abst) x4 x5
end of H12
suppose H13: eq T x0 x4
(H14)
consider H12
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) x0 x1 OF TSort ⇒x1 | TLRef ⇒x1 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abst) x4 x5 OF TSort ⇒x1 | TLRef ⇒x1 | THead t0⇒t0
that is equivalent to eq T x1 x5
by (eq_ind_r . . . H10 . previous)
∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t x1)
end of H14
(h1)
by (H14 . .)
pr3 (CHead c (Bind Abbr) x2) t x1
end of h1
(h2)
by (H6 . .)
pr3 (CHead c (Bind Abbr) x2) x1 x3
end of h2
by (pr3_t . . . h1 . h2)
we proved pr3 (CHead c (Bind Abbr) x2) t x3
by (pr3_head_12 . . . H4 . . . previous)
we proved pr3 c (THead (Bind Abbr) v t) (THead (Bind Abbr) x2 x3)
by (pr3_t . . . previous . H3)
we proved pr3 c (THead (Bind Abbr) v t) u2
(eq T x0 x4)→(pr3 c (THead (Bind Abbr) v t) u2)
end of h1
(h2)
consider H11
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) x0 x1 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abst) x4 x5 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0 ⇒t0
eq T x0 x4
end of h2
by (h1 h2)
pr3 c (THead (Bind Abbr) v t) u2
pr3 c (THead (Bind Abbr) v t) u2
pr3 c (THead (Bind Abbr) v t) u2
case or3_intro2 : H2: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.pr3 c (THead (Bind Abst) w t) (THead (Bind b) y1 z1) λb:B.λ:T.λ:T.λz2:T.λu3:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u3) z2)) u2 λ:B.λ:T.λ:T.λ:T.λu3:T.λ:T.pr3 c v u3 λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2 λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2 ⇒
the thesis becomes pr3 c (THead (Bind Abbr) v t) u2
we proceed by induction on H2 to prove pr3 c (THead (Bind Abbr) v t) u2
case ex6_6_intro : x0:B x1:T x2:T x3:T x4:T x5:T H3:not (eq B x0 Abst) H4:pr3 c (THead (Bind Abst) w t) (THead (Bind x0) x1 x2) H5:pr3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)) u2 :pr3 c v x4 :pr3 c x1 x5 H8:pr3 (CHead c (Bind x0) x5) x2 x3 ⇒
the thesis becomes pr3 c (THead (Bind Abbr) v t) u2
(H9)
by (pr3_gen_abst . . . . H4)
ex3_2
T
T
λu2:T.λt2:T.eq T (THead (Bind x0) x1 x2) (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c w u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t t2)
end of H9
we proceed by induction on H9 to prove pr3 c (THead (Bind Abbr) v t) u2
case ex3_2_intro : x6:T x7:T H10:eq T (THead (Bind x0) x1 x2) (THead (Bind Abst) x6 x7) H11:pr3 c w x6 H12:∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t x7) ⇒
the thesis becomes pr3 c (THead (Bind Abbr) v t) u2
(H13)
by (f_equal . . . . . H10)
we proved
eq
B
<λ:T.B>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒x0
| TLRef ⇒x0
| THead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x0
<λ:T.B>
CASE THead (Bind Abst) x6 x7 OF
TSort ⇒x0
| TLRef ⇒x0
| THead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x0
eq
B
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒x0
| TLRef ⇒x0
| THead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x0
THead (Bind x0) x1 x2
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒x0
| TLRef ⇒x0
| THead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x0
THead (Bind Abst) x6 x7
end of H13
(h1)
(H14)
by (f_equal . . . . . H10)
we proved
eq
T
<λ:T.T> CASE THead (Bind x0) x1 x2 OF TSort ⇒x1 | TLRef ⇒x1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abst) x6 x7 OF TSort ⇒x1 | TLRef ⇒x1 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x1 | TLRef ⇒x1 | THead t0 ⇒t0 (THead (Bind x0) x1 x2)
λe:T.<λ:T.T> CASE e OF TSort ⇒x1 | TLRef ⇒x1 | THead t0 ⇒t0
THead (Bind Abst) x6 x7
end of H14
(h1)
(H15)
by (f_equal . . . . . H10)
we proved
eq
T
<λ:T.T> CASE THead (Bind x0) x1 x2 OF TSort ⇒x2 | TLRef ⇒x2 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abst) x6 x7 OF TSort ⇒x2 | TLRef ⇒x2 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x2 | TLRef ⇒x2 | THead t0⇒t0 (THead (Bind x0) x1 x2)
λe:T.<λ:T.T> CASE e OF TSort ⇒x2 | TLRef ⇒x2 | THead t0⇒t0
THead (Bind Abst) x6 x7
end of H15
suppose H16: eq T x1 x6
suppose H17: eq B x0 Abst
(H22)
we proceed by induction on H17 to prove not (eq B Abst Abst)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
not (eq B Abst Abst)
end of H22
(H23)
by (refl_equal . .)
we proved eq B Abst Abst
by (H22 previous)
we proved False
by cases on the previous result we prove pr3 c (THead (Bind Abbr) v t) u2
pr3 c (THead (Bind Abbr) v t) u2
end of H23
consider H23
we proved pr3 c (THead (Bind Abbr) v t) u2
(eq T x1 x6)→(eq B x0 Abst)→(pr3 c (THead (Bind Abbr) v t) u2)
end of h1
(h2)
consider H14
we proved
eq
T
<λ:T.T> CASE THead (Bind x0) x1 x2 OF TSort ⇒x1 | TLRef ⇒x1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abst) x6 x7 OF TSort ⇒x1 | TLRef ⇒x1 | THead t0 ⇒t0
eq T x1 x6
end of h2
by (h1 h2)
(eq B x0 Abst)→(pr3 c (THead (Bind Abbr) v t) u2)
end of h1
(h2)
consider H13
we proved
eq
B
<λ:T.B>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒x0
| TLRef ⇒x0
| THead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x0
<λ:T.B>
CASE THead (Bind Abst) x6 x7 OF
TSort ⇒x0
| TLRef ⇒x0
| THead k ⇒<λ:K.B> CASE k OF Bind b⇒b | Flat ⇒x0
eq B x0 Abst
end of h2
by (h1 h2)
pr3 c (THead (Bind Abbr) v t) u2
pr3 c (THead (Bind Abbr) v t) u2
pr3 c (THead (Bind Abbr) v t) u2
we proved pr3 c (THead (Bind Abbr) v t) u2
we proved
∀c:C
.∀u2:T
.pr3 c (THead (Flat Appl) v (THead (Bind Abst) w t)) u2
→(iso (THead (Flat Appl) v (THead (Bind Abst) w t)) u2
→∀P:Prop.P
→pr3 c (THead (Bind Abbr) v t) u2)
that is equivalent to
let u1 := THead (Flat Appl) v (THead (Bind Abst) w t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THead (Bind Abbr) v t) u2)
we proved
∀v:T
.∀w:T
.∀t:T
.let u1 := THead (Flat Appl) v (THead (Bind Abst) w t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THead (Bind Abbr) v t) u2)