DEFINITION pr3_gen_bind()
TYPE =
∀b:B
.not (eq B b Abst)
→∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Bind b) u1 t1) x
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind b) u2 t2)
λu2:T.λ:T.pr3 c u1 u2
λ:T.λt2:T.pr3 (CHead c (Bind b) u1) t1 t2
pr3 (CHead c (Bind b) u1) t1 (lift (S O) O x))
BODY =
assume b: B
we proceed by induction on b to prove
not (eq B b Abst)
→∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Bind b) u1 t1) x
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind b) u2 t2)
λu2:T.λ:T.pr3 c u1 u2
λ:T.λt2:T.pr3 (CHead c (Bind b) u1) t1 t2
pr3 (CHead c (Bind b) u1) t1 (lift (S O) O x))
case Abbr : ⇒
the thesis becomes
not (eq B Abbr Abst)
→∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Bind Abbr) u1 t1) x
→(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))
suppose : not (eq B Abbr Abst)
assume c: C
assume u1: T
assume t1: T
assume x: T
suppose H0: pr3 c (THead (Bind Abbr) u1 t1) x
(H1)
by (pr3_gen_abbr . . . . H0)
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 H1
we proceed by induction on H1 to prove
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)
case or_introl : H2: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 ⇒
the thesis becomes
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)
we proceed by induction on H2 to prove
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)
case ex3_2_intro : x0:T x1:T H3:eq T x (THead (Bind Abbr) x0 x1) H4:pr3 c u1 x0 H5:pr3 (CHead c (Bind Abbr) u1) t1 x1 ⇒
the thesis becomes
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)
by (ex3_2_intro . . . . . . . H3 H4 H5)
we proved
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
by (or_introl . . previous)
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)
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)
case or_intror : H2:pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O x) ⇒
the thesis becomes
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)
by (or_intror . . 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)
we proved
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)
not (eq B Abbr Abst)
→∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Bind Abbr) u1 t1) x
→(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))
case Abst : ⇒
the thesis becomes
not (eq B Abst Abst)
→∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Bind Abst) u1 t1) x
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c u1 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abst) u1) t1 t2
pr3 (CHead c (Bind Abst) u1) t1 (lift (S O) O x))
suppose H: not (eq B Abst Abst)
assume c: C
assume u1: T
assume t1: T
assume x: T
suppose : pr3 c (THead (Bind Abst) u1 t1) x
(H1)
by (refl_equal . .)
we proved eq B Abst Abst
by (H previous)
we proved False
by cases on the previous result we prove
or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c u1 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abst) u1) t1 t2
pr3 (CHead c (Bind Abst) u1) t1 (lift (S O) O x)
or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c u1 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abst) u1) t1 t2
pr3 (CHead c (Bind Abst) u1) t1 (lift (S O) O x)
end of H1
consider H1
we proved
or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c u1 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abst) u1) t1 t2
pr3 (CHead c (Bind Abst) u1) t1 (lift (S O) O x)
not (eq B Abst Abst)
→∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Bind Abst) u1 t1) x
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c u1 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abst) u1) t1 t2
pr3 (CHead c (Bind Abst) u1) t1 (lift (S O) O x))
case Void : ⇒
the thesis becomes
not (eq B Void Abst)
→∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Bind Void) u1 t1) x
→(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.pr3 (CHead c (Bind Void) u1) t1 t2
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x))
suppose : not (eq B Void Abst)
assume c: C
assume u1: T
assume t1: T
assume x: T
suppose H0: pr3 c (THead (Bind Void) u1 t1) x
(H1)
by (pr3_gen_void . . . . H0)
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 H1
we proceed by induction on H1 to prove
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.pr3 (CHead c (Bind Void) u1) t1 t2
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)
case or_introl : H2: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.∀b0:B.∀u:T.(pr3 (CHead c (Bind b0) u) t1 t2) ⇒
the thesis becomes
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.pr3 (CHead c (Bind Void) u1) t1 t2
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)
we proceed by induction on H2 to prove
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.pr3 (CHead c (Bind Void) u1) t1 t2
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)
case ex3_2_intro : x0:T x1:T H3:eq T x (THead (Bind Void) x0 x1) H4:pr3 c u1 x0 H5:∀b0:B.∀u:T.(pr3 (CHead c (Bind b0) u) t1 x1) ⇒
the thesis becomes
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.pr3 (CHead c (Bind Void) u1) t1 t2
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)
by (H5 . .)
we proved pr3 (CHead c (Bind Void) u1) t1 x1
by (ex3_2_intro . . . . . . . H3 H4 previous)
we proved
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.pr3 (CHead c (Bind Void) u1) t1 t2
by (or_introl . . previous)
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.pr3 (CHead c (Bind Void) u1) t1 t2
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)
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.pr3 (CHead c (Bind Void) u1) t1 t2
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)
case or_intror : H2:pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x) ⇒
the thesis becomes
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.pr3 (CHead c (Bind Void) u1) t1 t2
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)
by (or_intror . . 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.pr3 (CHead c (Bind Void) u1) t1 t2
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)
we proved
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.pr3 (CHead c (Bind Void) u1) t1 t2
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)
not (eq B Void Abst)
→∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Bind Void) u1 t1) x
→(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.pr3 (CHead c (Bind Void) u1) t1 t2
pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x))
we proved
not (eq B b Abst)
→∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Bind b) u1 t1) x
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind b) u2 t2)
λu2:T.λ:T.pr3 c u1 u2
λ:T.λt2:T.pr3 (CHead c (Bind b) u1) t1 t2
pr3 (CHead c (Bind b) u1) t1 (lift (S O) O x))
we proved
∀b:B
.not (eq B b Abst)
→∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Bind b) u1 t1) x
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind b) u2 t2)
λu2:T.λ:T.pr3 c u1 u2
λ:T.λt2:T.pr3 (CHead c (Bind b) u1) t1 t2
pr3 (CHead c (Bind b) u1) t1 (lift (S O) O x))