DEFINITION pc3_gen_not_abst()
TYPE =
∀b:B
.not (eq B b Abst)
→∀c:C
.∀t1:T
.∀t2:T
.∀u1:T
.∀u2:T
.pc3 c (THead (Bind b) u1 t1) (THead (Bind Abst) u2 t2)
→pc3 (CHead c (Bind b) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
BODY =
assume b: B
we proceed by induction on b to prove
not (eq B b Abst)
→∀c:C
.∀t1:T
.∀t2:T
.∀u1:T
.∀u2:T
.pc3 c (THead (Bind b) u1 t1) (THead (Bind Abst) u2 t2)
→pc3 (CHead c (Bind b) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case Abbr : ⇒
the thesis becomes
not (eq B Abbr Abst)
→∀c:C
.∀t1:T
.∀t2:T
.∀u1:T
.∀u2:T
.pc3 c (THead (Bind Abbr) u1 t1) (THead (Bind Abst) u2 t2)
→pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
suppose : not (eq B Abbr Abst)
assume c: C
assume t1: T
assume t2: T
assume u1: T
assume u2: T
suppose H0: pc3 c (THead (Bind Abbr) u1 t1) (THead (Bind Abst) u2 t2)
(H1) consider H0
consider H1
we proved pc3 c (THead (Bind Abbr) u1 t1) (THead (Bind Abst) u2 t2)
that is equivalent to
ex2
T
λt:T.pr3 c (THead (Bind Abbr) u1 t1) t
λt:T.pr3 c (THead (Bind Abst) u2 t2) t
we proceed by induction on the previous result to prove
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case ex_intro2 : x:T H2:pr3 c (THead (Bind Abbr) u1 t1) x H3:pr3 c (THead (Bind Abst) u2 t2) x ⇒
the thesis becomes
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
(H4)
by (pr3_gen_abbr . . . . H2)
or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.pr3 c u1 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abbr) u1) t1 t2
pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O x)
end of H4
we proceed by induction on H4 to prove
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case or_introl : H5:ex3_2 T T λu3:T.λt3:T.eq T x (THead (Bind Abbr) u3 t3) λu3:T.λ:T.pr3 c u1 u3 λ:T.λt3:T.pr3 (CHead c (Bind Abbr) u1) t1 t3 ⇒
the thesis becomes
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
we proceed by induction on H5 to prove
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case ex3_2_intro : x0:T x1:T H6:eq T x (THead (Bind Abbr) x0 x1) :pr3 c u1 x0 :pr3 (CHead c (Bind Abbr) u1) t1 x1 ⇒
the thesis becomes
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
(H9)
by (pr3_gen_abst . . . . H3)
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c u2 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 t2)
end of H9
we proceed by induction on H9 to prove
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case ex3_2_intro : x2:T x3:T H10:eq T x (THead (Bind Abst) x2 x3) :pr3 c u2 x2 :∀b0:B.∀u:T.(pr3 (CHead c (Bind b0) u) t2 x3) ⇒
the thesis becomes
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
(H13)
we proceed by induction on H10 to prove eq T (THead (Bind Abst) x2 x3) (THead (Bind Abbr) x0 x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H6
eq T (THead (Bind Abst) x2 x3) (THead (Bind Abbr) x0 x1)
end of H13
(H14)
we proceed by induction on H13 to prove
<λ:T.Prop>
CASE THead (Bind Abbr) x0 x1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind Abst) x2 x3 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind Abst) x2 x3 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
<λ:T.Prop>
CASE THead (Bind Abbr) x0 x1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
end of H14
consider H14
we proved
<λ:T.Prop>
CASE THead (Bind Abbr) x0 x1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case or_intror : H5:pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O x) ⇒
the thesis becomes
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
(H6)
by (pr3_gen_abst . . . . H3)
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c u2 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 t2)
end of H6
we proceed by induction on H6 to prove
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case ex3_2_intro : x0:T x1:T H7:eq T x (THead (Bind Abst) x0 x1) H8:pr3 c u2 x0 H9:∀b0:B.∀u:T.(pr3 (CHead c (Bind b0) u) t2 x1) ⇒
the thesis becomes
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
(H10)
we proceed by induction on H7 to prove
pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) x0 x1))
case refl_equal : ⇒
the thesis becomes the hypothesis H5
pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) x0 x1))
end of H10
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind Abbr) O) O c c
by (drop_drop . . . . previous .)
drop (S O) O (CHead c (Bind Abbr) u1) c
end of h1
(h2)
by (H9 . .)
we proved pr3 (CHead c (Bind Abst) x0) t2 x1
by (pr3_head_12 . . . H8 . . . previous)
pr3 c (THead (Bind Abst) u2 t2) (THead (Bind Abst) x0 x1)
end of h2
by (pr3_lift . . . . h1 . . h2)
we proved
pr3
CHead c (Bind Abbr) u1
lift (S O) O (THead (Bind Abst) u2 t2)
lift (S O) O (THead (Bind Abst) x0 x1)
by (pc3_pr3_t . . . H10 . previous)
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
we proved
pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
not (eq B Abbr Abst)
→∀c:C
.∀t1:T
.∀t2:T
.∀u1:T
.∀u2:T
.pc3 c (THead (Bind Abbr) u1 t1) (THead (Bind Abst) u2 t2)
→pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case Abst : ⇒
the thesis becomes
not (eq B Abst Abst)
→∀c:C
.∀t1:T
.∀t2:T
.∀u1:T
.∀u2:T
.pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)
→pc3 (CHead c (Bind Abst) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
suppose H: not (eq B Abst Abst)
assume c: C
assume t1: T
assume t2: T
assume u1: T
assume u2: T
suppose : pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)
(H1)
by (refl_equal . .)
we proved eq B Abst Abst
by (H previous)
we proved False
by cases on the previous result we prove
pc3 (CHead c (Bind Abst) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
pc3 (CHead c (Bind Abst) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
end of H1
consider H1
we proved
pc3 (CHead c (Bind Abst) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
not (eq B Abst Abst)
→∀c:C
.∀t1:T
.∀t2:T
.∀u1:T
.∀u2:T
.pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)
→pc3 (CHead c (Bind Abst) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case Void : ⇒
the thesis becomes
not (eq B Void Abst)
→∀c:C
.∀t1:T
.∀t2:T
.∀u1:T
.∀u2:T
.pc3 c (THead (Bind Void) u1 t1) (THead (Bind Abst) u2 t2)
→pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
suppose : not (eq B Void Abst)
assume c: C
assume t1: T
assume t2: T
assume u1: T
assume u2: T
suppose H0: pc3 c (THead (Bind Void) u1 t1) (THead (Bind Abst) u2 t2)
(H1) consider H0
consider H1
we proved pc3 c (THead (Bind Void) u1 t1) (THead (Bind Abst) u2 t2)
that is equivalent to
ex2
T
λt:T.pr3 c (THead (Bind Void) u1 t1) t
λt:T.pr3 c (THead (Bind Abst) u2 t2) t
we proceed by induction on the previous result to prove
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case ex_intro2 : x:T H2:pr3 c (THead (Bind Void) u1 t1) x H3:pr3 c (THead (Bind Abst) u2 t2) x ⇒
the thesis becomes
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
(H4)
by (pr3_gen_void . . . . H2)
or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Void) u2 t2)
λu2:T.λ:T.pr3 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t1 t2)
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)
end of H4
we proceed by induction on H4 to prove
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case or_introl : H5:ex3_2 T T λu3:T.λt3:T.eq T x (THead (Bind Void) u3 t3) λu3:T.λ:T.pr3 c u1 u3 λ:T.λt3:T.∀b0:B.∀u:T.(pr3 (CHead c (Bind b0) u) t1 t3) ⇒
the thesis becomes
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
we proceed by induction on H5 to prove
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case ex3_2_intro : x0:T x1:T H6:eq T x (THead (Bind Void) x0 x1) :pr3 c u1 x0 :∀b0:B.∀u:T.(pr3 (CHead c (Bind b0) u) t1 x1) ⇒
the thesis becomes
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
(H9)
by (pr3_gen_abst . . . . H3)
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c u2 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 t2)
end of H9
we proceed by induction on H9 to prove
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case ex3_2_intro : x2:T x3:T H10:eq T x (THead (Bind Abst) x2 x3) :pr3 c u2 x2 :∀b0:B.∀u:T.(pr3 (CHead c (Bind b0) u) t2 x3) ⇒
the thesis becomes
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
(H13)
we proceed by induction on H10 to prove eq T (THead (Bind Abst) x2 x3) (THead (Bind Void) x0 x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H6
eq T (THead (Bind Abst) x2 x3) (THead (Bind Void) x0 x1)
end of H13
(H14)
we proceed by induction on H13 to prove
<λ:T.Prop>
CASE THead (Bind Void) x0 x1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind Abst) x2 x3 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind Abst) x2 x3 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
<λ:T.Prop>
CASE THead (Bind Void) x0 x1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
end of H14
consider H14
we proved
<λ:T.Prop>
CASE THead (Bind Void) x0 x1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind b0⇒<λ:B.Prop> CASE b0 OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case or_intror : H5:pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x) ⇒
the thesis becomes
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
(H6)
by (pr3_gen_abst . . . . H3)
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c u2 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 t2)
end of H6
we proceed by induction on H6 to prove
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
case ex3_2_intro : x0:T x1:T H7:eq T x (THead (Bind Abst) x0 x1) H8:pr3 c u2 x0 H9:∀b0:B.∀u:T.(pr3 (CHead c (Bind b0) u) t2 x1) ⇒
the thesis becomes
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
(H10)
we proceed by induction on H7 to prove
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) x0 x1))
case refl_equal : ⇒
the thesis becomes the hypothesis H5
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) x0 x1))
end of H10
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind Void) O) O c c
by (drop_drop . . . . previous .)
drop (S O) O (CHead c (Bind Void) u1) c
end of h1
(h2)
by (H9 . .)
we proved pr3 (CHead c (Bind Abst) x0) t2 x1
by (pr3_head_12 . . . H8 . . . previous)
pr3 c (THead (Bind Abst) u2 t2) (THead (Bind Abst) x0 x1)
end of h2
by (pr3_lift . . . . h1 . . h2)
we proved
pr3
CHead c (Bind Void) u1
lift (S O) O (THead (Bind Abst) u2 t2)
lift (S O) O (THead (Bind Abst) x0 x1)
by (pc3_pr3_t . . . H10 . previous)
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
we proved
pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
not (eq B Void Abst)
→∀c:C
.∀t1:T
.∀t2:T
.∀u1:T
.∀u2:T
.pc3 c (THead (Bind Void) u1 t1) (THead (Bind Abst) u2 t2)
→pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
we proved
not (eq B b Abst)
→∀c:C
.∀t1:T
.∀t2:T
.∀u1:T
.∀u2:T
.pc3 c (THead (Bind b) u1 t1) (THead (Bind Abst) u2 t2)
→pc3 (CHead c (Bind b) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
we proved
∀b:B
.not (eq B b Abst)
→∀c:C
.∀t1:T
.∀t2:T
.∀u1:T
.∀u2:T
.pc3 c (THead (Bind b) u1 t1) (THead (Bind Abst) u2 t2)
→pc3 (CHead c (Bind b) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))