DEFINITION pc3_gen_abst()
TYPE =
∀c:C
.∀u1:T
.∀u2:T
.∀t1:T
.∀t2:T
.pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)
→land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
BODY =
assume c: C
assume u1: T
assume u2: T
assume t1: T
assume t2: T
suppose H: pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)
(H0) consider H
consider H0
we proved pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)
that is equivalent to
ex2
T
λt:T.pr3 c (THead (Bind Abst) u1 t1) t
λt:T.pr3 c (THead (Bind Abst) u2 t2) t
we proceed by induction on the previous result to prove land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
case ex_intro2 : x:T H1:pr3 c (THead (Bind Abst) u1 t1) x H2:pr3 c (THead (Bind Abst) u2 t2) x ⇒
the thesis becomes land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
(H3)
by (pr3_gen_abst . . . . H2)
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 H3
we proceed by induction on H3 to prove land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
case ex3_2_intro : x0:T x1:T H4:eq T x (THead (Bind Abst) x0 x1) H5:pr3 c u2 x0 H6:∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 x1) ⇒
the thesis becomes land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
(H7)
by (pr3_gen_abst . . . . H1)
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.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t1 t2)
end of H7
we proceed by induction on H7 to prove land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
case ex3_2_intro : x2:T x3:T H8:eq T x (THead (Bind Abst) x2 x3) H9:pr3 c u1 x2 H10:∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t1 x3) ⇒
the thesis becomes land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
(H11)
we proceed by induction on H8 to prove eq T (THead (Bind Abst) x2 x3) (THead (Bind Abst) x0 x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq T (THead (Bind Abst) x2 x3) (THead (Bind Abst) x0 x1)
end of H11
(H12)
by (f_equal . . . . . H11)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) x2 x3 OF TSort ⇒x2 | TLRef ⇒x2 | THead t ⇒t
<λ:T.T> CASE THead (Bind Abst) x0 x1 OF TSort ⇒x2 | TLRef ⇒x2 | THead t ⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x2 | TLRef ⇒x2 | THead t ⇒t
THead (Bind Abst) x2 x3
λe:T.<λ:T.T> CASE e OF TSort ⇒x2 | TLRef ⇒x2 | THead t ⇒t
THead (Bind Abst) x0 x1
end of H12
(h1)
(H13)
by (f_equal . . . . . H11)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) x2 x3 OF TSort ⇒x3 | TLRef ⇒x3 | THead t⇒t
<λ:T.T> CASE THead (Bind Abst) x0 x1 OF TSort ⇒x3 | TLRef ⇒x3 | THead t⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x3 | TLRef ⇒x3 | THead t⇒t
THead (Bind Abst) x2 x3
λe:T.<λ:T.T> CASE e OF TSort ⇒x3 | TLRef ⇒x3 | THead t⇒t
THead (Bind Abst) x0 x1
end of H13
suppose H14: eq T x2 x0
(H15)
consider H13
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) x2 x3 OF TSort ⇒x3 | TLRef ⇒x3 | THead t⇒t
<λ:T.T> CASE THead (Bind Abst) x0 x1 OF TSort ⇒x3 | TLRef ⇒x3 | THead t⇒t
that is equivalent to eq T x3 x1
we proceed by induction on the previous result to prove ∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t1 x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H10
∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t1 x1)
end of H15
(H16)
we proceed by induction on H14 to prove pr3 c u1 x0
case refl_equal : ⇒
the thesis becomes the hypothesis H9
pr3 c u1 x0
end of H16
(h1)
by (pc3_pr3_t . . . H16 . H5)
pc3 c u1 u2
end of h1
(h2)
assume b: B
assume u: T
(h1)
by (H15 . .)
pr3 (CHead c (Bind b) u) t1 x1
end of h1
(h2)
by (H6 . .)
pr3 (CHead c (Bind b) u) t2 x1
end of h2
by (pc3_pr3_t . . . h1 . h2)
we proved pc3 (CHead c (Bind b) u) t1 t2
∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
end of h2
by (conj . . h1 h2)
we proved land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
(eq T x2 x0)→(land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2))
end of h1
(h2)
consider H12
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) x2 x3 OF TSort ⇒x2 | TLRef ⇒x2 | THead t ⇒t
<λ:T.T> CASE THead (Bind Abst) x0 x1 OF TSort ⇒x2 | TLRef ⇒x2 | THead t ⇒t
eq T x2 x0
end of h2
by (h1 h2)
land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
we proved land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
we proved
∀c:C
.∀u1:T
.∀u2:T
.∀t1:T
.∀t2:T
.pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)
→land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)