DEFINITION pr3_iso_appl_bind()
TYPE =
∀b:B
.not (eq B b Abst)
→∀v1:T
.∀v2:T
.∀t:T
.let u1 := THead (Flat Appl) v1 (THead (Bind b) v2 t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2)
BODY =
assume b: B
suppose H: not (eq B b Abst)
assume v1: T
assume v2: T
assume t: T
we must prove
let u1 := THead (Flat Appl) v1 (THead (Bind b) v2 t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2)
or equivalently
∀c:C
.∀u2:T
.pr3 c (THead (Flat Appl) v1 (THead (Bind b) v2 t)) u2
→((iso (THead (Flat Appl) v1 (THead (Bind b) v2 t)) u2)→∀P:Prop.P
→pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2)
assume c: C
assume u2: T
suppose H0: pr3 c (THead (Flat Appl) v1 (THead (Bind b) v2 t)) u2
suppose H1: (iso (THead (Flat Appl) v1 (THead (Bind b) v2 t)) u2)→∀P:Prop.P
(H2)
by (pr3_gen_appl . . . . H0)
or3
ex3_2
T
T
λu2:T.λt2:T.eq T u2 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr3 c v1 u2
λ:T.λt2:T.pr3 c (THead (Bind b) v2 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 v1 u2
λy1:T.λz1:T.λ:T.λ:T.pr3 c (THead (Bind b) v2 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 b) v2 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 v1 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 H2
we proceed by induction on H2 to prove pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
case or3_intro0 : H3:ex3_2 T T λu3:T.λt2:T.eq T u2 (THead (Flat Appl) u3 t2) λu3:T.λ:T.pr3 c v1 u3 λ:T.λt2:T.pr3 c (THead (Bind b) v2 t) t2 ⇒
the thesis becomes pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
we proceed by induction on H3 to prove pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
case ex3_2_intro : x0:T x1:T H4:eq T u2 (THead (Flat Appl) x0 x1) :pr3 c v1 x0 :pr3 c (THead (Bind b) v2 t) x1 ⇒
the thesis becomes pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
(H7)
we proceed by induction on H4 to prove
(iso
THead (Flat Appl) v1 (THead (Bind b) v2 t)
THead (Flat Appl) x0 x1)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H1
(iso
THead (Flat Appl) v1 (THead (Bind b) v2 t)
THead (Flat Appl) x0 x1)
→∀P:Prop.P
end of H7
by (iso_head . . . . .)
we proved
iso
THead (Flat Appl) v1 (THead (Bind b) v2 t)
THead (Flat Appl) x0 x1
by (H7 previous .)
we proved
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Flat Appl) x0 x1
by (eq_ind_r . . . previous . H4)
pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
case or3_intro1 : H3: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 v1 u3 λy1:T.λz1:T.λ:T.λ:T.pr3 c (THead (Bind b) v2 t) (THead (Bind Abst) y1 z1) λ:T.λz1:T.λ:T.λt2:T.∀b0:B.∀u:T.(pr3 (CHead c (Bind b0) u) z1 t2) ⇒
the thesis becomes pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
we proceed by induction on H3 to prove pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
case ex4_4_intro : x0:T x1:T x2:T x3:T H4:pr3 c (THead (Bind Abbr) x2 x3) u2 H5:pr3 c v1 x2 H6:pr3 c (THead (Bind b) v2 t) (THead (Bind Abst) x0 x1) H7:∀b0:B.∀u:T.(pr3 (CHead c (Bind b0) u) x1 x3) ⇒
the thesis becomes pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
(H_x)
by (pr3_gen_bind . H . . . . H6)
or
ex3_2
T
T
λu2:T.λt2:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind b) u2 t2)
λu2:T.λ:T.pr3 c v2 u2
λ:T.λt2:T.pr3 (CHead c (Bind b) v2) t t2
pr3 (CHead c (Bind b) v2) t (lift (S O) O (THead (Bind Abst) x0 x1))
end of H_x
(H8) consider H_x
we proceed by induction on H8 to prove
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
case or_introl : H9:ex3_2 T T λu3:T.λt2:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind b) u3 t2) λu3:T.λ:T.pr3 c v2 u3 λ:T.λt2:T.pr3 (CHead c (Bind b) v2) t t2 ⇒
the thesis becomes
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
we proceed by induction on H9 to prove
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
case ex3_2_intro : x4:T x5:T H10:eq T (THead (Bind Abst) x0 x1) (THead (Bind b) x4 x5) H11:pr3 c v2 x4 H12:pr3 (CHead c (Bind b) v2) t x5 ⇒
the thesis becomes
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
(H13)
by (f_equal . . . . . H10)
we proved
eq
B
<λ:T.B>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒Abst
| TLRef ⇒Abst
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abst
<λ:T.B>
CASE THead (Bind b) x4 x5 OF
TSort ⇒Abst
| TLRef ⇒Abst
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abst
eq
B
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒Abst
| TLRef ⇒Abst
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abst
THead (Bind Abst) x0 x1
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒Abst
| TLRef ⇒Abst
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abst
THead (Bind b) x4 x5
end of H13
(h1)
(H14)
by (f_equal . . . . . H10)
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 b) 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 b) x4 x5)
end of H14
(h1)
(H15)
by (f_equal . . . . . H10)
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 b) 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 b) x4 x5)
end of H15
suppose H16: eq T x0 x4
suppose H17: eq B Abst b
(H18)
consider H15
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 b) x4 x5 OF TSort ⇒x1 | TLRef ⇒x1 | THead t0⇒t0
that is equivalent to eq T x1 x5
by (eq_ind_r . . . H12 . previous)
pr3 (CHead c (Bind b) v2) t x1
end of H18
(H21)
by (eq_ind_r . . . H . H17)
not (eq B Abst Abst)
end of H21
we proceed by induction on H17 to prove
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
case refl_equal : ⇒
the thesis becomes
pr3
c
THead (Bind Abst) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
(H22)
by (refl_equal . .)
we proved eq B Abst Abst
by (H21 previous)
we proved False
by cases on the previous result we prove
pr3
c
THead (Bind Abst) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
pr3
c
THead (Bind Abst) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
end of H22
consider H22
pr3
c
THead (Bind Abst) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
we proved
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
eq T x0 x4
→(eq B Abst b
→(pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3))
end of h1
(h2)
consider H14
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 b) x4 x5 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0 ⇒t0
eq T x0 x4
end of h2
by (h1 h2)
eq B Abst b
→(pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3)
end of h1
(h2)
consider H13
we proved
eq
B
<λ:T.B>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒Abst
| TLRef ⇒Abst
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abst
<λ:T.B>
CASE THead (Bind b) x4 x5 OF
TSort ⇒Abst
| TLRef ⇒Abst
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abst
eq B Abst b
end of h2
by (h1 h2)
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
case or_intror : H9:pr3 (CHead c (Bind b) v2) t (lift (S O) O (THead (Bind Abst) x0 x1)) ⇒
the thesis becomes
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind b) O) O c c
by (drop_drop . . . . previous .)
we proved drop (S O) O (CHead c (Bind b) v2) c
by (pr3_lift . . . . previous . . H5)
we proved pr3 (CHead c (Bind b) v2) (lift (S O) O v1) (lift (S O) O x2)
by (pr3_flat . . . previous . . H9 .)
we proved
pr3
CHead c (Bind b) v2
THead (Flat Appl) (lift (S O) O v1) t
THead
Flat Appl
lift (S O) O x2
lift (S O) O (THead (Bind Abst) x0 x1)
by (pr3_head_2 . . . . . previous)
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead
Bind b
v2
THead
Flat Appl
lift (S O) O x2
lift (S O) O (THead (Bind Abst) x0 x1)
end of h1
(h2)
by (lift_flat . . . . .)
we proved
eq
T
lift (S O) O (THead (Flat Appl) x2 (THead (Bind Abst) x0 x1))
THead
Flat Appl
lift (S O) O x2
lift (S O) O (THead (Bind Abst) x0 x1)
we proceed by induction on the previous result to prove
pr3
c
THead
Bind b
v2
THead
Flat Appl
lift (S O) O x2
lift (S O) O (THead (Bind Abst) x0 x1)
THead (Bind Abbr) x2 x3
case refl_equal : ⇒
the thesis becomes
pr3
c
THead
Bind b
v2
lift (S O) O (THead (Flat Appl) x2 (THead (Bind Abst) x0 x1))
THead (Bind Abbr) x2 x3
(h1)
(h1) by (pr0_refl .) we proved pr0 x2 x2
(h2) by (pr0_refl .) we proved pr0 x1 x1
by (pr0_beta . . . h1 . . h2)
we proved
pr0
THead (Flat Appl) x2 (THead (Bind Abst) x0 x1)
THead (Bind Abbr) x2 x1
by (pr0_zeta . H . . previous .)
we proved
pr0
THead
Bind b
v2
lift (S O) O (THead (Flat Appl) x2 (THead (Bind Abst) x0 x1))
THead (Bind Abbr) x2 x1
by (pr2_free . . . previous)
pr2
c
THead
Bind b
v2
lift (S O) O (THead (Flat Appl) x2 (THead (Bind Abst) x0 x1))
THead (Bind Abbr) x2 x1
end of h1
(h2)
(h1) by (pr3_refl . .) we proved pr3 c x2 x2
(h2)
by (H7 . .)
pr3 (CHead c (Bind Abbr) x2) x1 x3
end of h2
by (pr3_head_12 . . . h1 . . . h2)
pr3 c (THead (Bind Abbr) x2 x1) (THead (Bind Abbr) x2 x3)
end of h2
by (pr3_sing . . . h1 . h2)
pr3
c
THead
Bind b
v2
lift (S O) O (THead (Flat Appl) x2 (THead (Bind Abst) x0 x1))
THead (Bind Abbr) x2 x3
pr3
c
THead
Bind b
v2
THead
Flat Appl
lift (S O) O x2
lift (S O) O (THead (Bind Abst) x0 x1)
THead (Bind Abbr) x2 x3
end of h2
by (pr3_t . . . h1 . h2)
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
we proved
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind Abbr) x2 x3
by (pr3_t . . . previous . H4)
pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
case or3_intro2 : H3:ex6_6 B T T T T T λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst) λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c (THead (Bind b) v2 t) (THead (Bind b0) y1 z1) λb0:B.λ:T.λ:T.λz2:T.λu3:T.λy2:T.pr3 c (THead (Bind b0) y2 (THead (Flat Appl) (lift (S O) O u3) z2)) u2 λ:B.λ:T.λ:T.λ:T.λu3:T.λ:T.pr3 c v1 u3 λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2 λb0:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b0) y2) z1 z2 ⇒
the thesis becomes pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
we proceed by induction on H3 to prove pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
case ex6_6_intro : x0:B x1:T x2:T x3:T x4:T x5:T H4:not (eq B x0 Abst) H5:pr3 c (THead (Bind b) v2 t) (THead (Bind x0) x1 x2) H6:pr3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)) u2 H7:pr3 c v1 x4 H8:pr3 c x1 x5 H9:pr3 (CHead c (Bind x0) x5) x2 x3 ⇒
the thesis becomes pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
(H_x)
by (pr3_gen_bind . H . . . . H5)
or
ex3_2
T
T
λu2:T.λt2:T.eq T (THead (Bind x0) x1 x2) (THead (Bind b) u2 t2)
λu2:T.λ:T.pr3 c v2 u2
λ:T.λt2:T.pr3 (CHead c (Bind b) v2) t t2
pr3 (CHead c (Bind b) v2) t (lift (S O) O (THead (Bind x0) x1 x2))
end of H_x
(H10) consider H_x
we proceed by induction on H10 to prove
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
case or_introl : H11:ex3_2 T T λu3:T.λt2:T.eq T (THead (Bind x0) x1 x2) (THead (Bind b) u3 t2) λu3:T.λ:T.pr3 c v2 u3 λ:T.λt2:T.pr3 (CHead c (Bind b) v2) t t2 ⇒
the thesis becomes
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
we proceed by induction on H11 to prove
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
case ex3_2_intro : x6:T x7:T H12:eq T (THead (Bind x0) x1 x2) (THead (Bind b) x6 x7) H13:pr3 c v2 x6 H14:pr3 (CHead c (Bind b) v2) t x7 ⇒
the thesis becomes
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
(H15)
by (f_equal . . . . . H12)
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 b0⇒b0 | Flat ⇒x0
<λ:T.B>
CASE THead (Bind b) x6 x7 OF
TSort ⇒x0
| TLRef ⇒x0
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒x0
eq
B
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒x0
| TLRef ⇒x0
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | 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 b0⇒b0 | Flat ⇒x0
THead (Bind b) x6 x7
end of H15
(h1)
(H16)
by (f_equal . . . . . H12)
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 b) 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 b) x6 x7)
end of H16
(h1)
(H17)
by (f_equal . . . . . H12)
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 b) 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 b) x6 x7)
end of H17
suppose H18: eq T x1 x6
suppose H19: eq B x0 b
(H20)
consider H17
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 b) x6 x7 OF TSort ⇒x2 | TLRef ⇒x2 | THead t0⇒t0
that is equivalent to eq T x2 x7
by (eq_ind_r . . . H14 . previous)
pr3 (CHead c (Bind b) v2) t x2
end of H20
(H21)
by (eq_ind_r . . . H13 . H18)
pr3 c v2 x1
end of H21
(H22)
we proceed by induction on H19 to prove pr3 (CHead c (Bind b) x5) x2 x3
case refl_equal : ⇒
the thesis becomes the hypothesis H9
pr3 (CHead c (Bind b) x5) x2 x3
end of H22
(h1) by (pr3_t . . . H21 . H8) we proved pr3 c v2 x5
(h2)
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind b) O) O c c
by (drop_drop . . . . previous .)
we proved drop (S O) O (CHead c (Bind b) v2) c
by (pr3_lift . . . . previous . . H7)
pr3 (CHead c (Bind b) v2) (lift (S O) O v1) (lift (S O) O x4)
end of h1
(h2)
by (pr3_pr3_pr3_t . . . H8 . . . H22)
we proved pr3 (CHead c (Bind b) x1) x2 x3
by (pr3_pr3_pr3_t . . . H21 . . . previous)
we proved pr3 (CHead c (Bind b) v2) x2 x3
by (pr3_t . . . H20 . previous)
pr3 (CHead c (Bind b) v2) t x3
end of h2
by (pr3_flat . . . h1 . . h2 .)
pr3
CHead c (Bind b) v2
THead (Flat Appl) (lift (S O) O v1) t
THead (Flat Appl) (lift (S O) O x4) x3
end of h2
by (pr3_head_21 . . . h1 . . . h2)
we proved
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind b) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
by (eq_ind_r . . . previous . H19)
we proved
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
eq T x1 x6
→(eq B x0 b
→(pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)))
end of h1
(h2)
consider H16
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 b) x6 x7 OF TSort ⇒x1 | TLRef ⇒x1 | THead t0 ⇒t0
eq T x1 x6
end of h2
by (h1 h2)
eq B x0 b
→(pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))
end of h1
(h2)
consider H15
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 b0⇒b0 | Flat ⇒x0
<λ:T.B>
CASE THead (Bind b) x6 x7 OF
TSort ⇒x0
| TLRef ⇒x0
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒x0
eq B x0 b
end of h2
by (h1 h2)
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
case or_intror : H11:pr3 (CHead c (Bind b) v2) t (lift (S O) O (THead (Bind x0) x1 x2)) ⇒
the thesis becomes
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind b) O) O c c
by (drop_drop . . . . previous .)
we proved drop (S O) O (CHead c (Bind b) v2) c
by (pr3_lift . . . . previous . . H7)
we proved pr3 (CHead c (Bind b) v2) (lift (S O) O v1) (lift (S O) O x4)
by (pr3_flat . . . previous . . H11 .)
we proved
pr3
CHead c (Bind b) v2
THead (Flat Appl) (lift (S O) O v1) t
THead
Flat Appl
lift (S O) O x4
lift (S O) O (THead (Bind x0) x1 x2)
by (pr3_head_2 . . . . . previous)
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead
Bind b
v2
THead
Flat Appl
lift (S O) O x4
lift (S O) O (THead (Bind x0) x1 x2)
end of h1
(h2)
by (lift_flat . . . . .)
we proved
eq
T
lift (S O) O (THead (Flat Appl) x4 (THead (Bind x0) x1 x2))
THead
Flat Appl
lift (S O) O x4
lift (S O) O (THead (Bind x0) x1 x2)
we proceed by induction on the previous result to prove
pr3
c
THead
Bind b
v2
THead
Flat Appl
lift (S O) O x4
lift (S O) O (THead (Bind x0) x1 x2)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
case refl_equal : ⇒
the thesis becomes
pr3
c
THead
Bind b
v2
lift (S O) O (THead (Flat Appl) x4 (THead (Bind x0) x1 x2))
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
(h1)
(h1) by (pr0_refl .) we proved pr0 x4 x4
(h2) by (pr0_refl .) we proved pr0 x1 x1
(h3) by (pr0_refl .) we proved pr0 x2 x2
by (pr0_upsilon . H4 . . h1 . . h2 . . h3)
we proved
pr0
THead (Flat Appl) x4 (THead (Bind x0) x1 x2)
THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)
by (pr0_zeta . H . . previous .)
we proved
pr0
THead
Bind b
v2
lift (S O) O (THead (Flat Appl) x4 (THead (Bind x0) x1 x2))
THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)
by (pr2_free . . . previous)
pr2
c
THead
Bind b
v2
lift (S O) O (THead (Flat Appl) x4 (THead (Bind x0) x1 x2))
THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)
end of h1
(h2)
by (pr3_thin_dx . . . H9 . .)
we proved
pr3
CHead c (Bind x0) x5
THead (Flat Appl) (lift (S O) O x4) x2
THead (Flat Appl) (lift (S O) O x4) x3
by (pr3_head_12 . . . H8 . . . previous)
pr3
c
THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
end of h2
by (pr3_sing . . . h1 . h2)
pr3
c
THead
Bind b
v2
lift (S O) O (THead (Flat Appl) x4 (THead (Bind x0) x1 x2))
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
pr3
c
THead
Bind b
v2
THead
Flat Appl
lift (S O) O x4
lift (S O) O (THead (Bind x0) x1 x2)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
end of h2
by (pr3_t . . . h1 . h2)
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
we proved
pr3
c
THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
by (pr3_t . . . previous . H6)
pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
we proved pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2
we proved
∀c:C
.∀u2:T
.pr3 c (THead (Flat Appl) v1 (THead (Bind b) v2 t)) u2
→((iso (THead (Flat Appl) v1 (THead (Bind b) v2 t)) u2)→∀P:Prop.P
→pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2)
that is equivalent to
let u1 := THead (Flat Appl) v1 (THead (Bind b) v2 t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2)
we proved
∀b:B
.not (eq B b Abst)
→∀v1:T
.∀v2:T
.∀t:T
.let u1 := THead (Flat Appl) v1 (THead (Bind b) v2 t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2)