DEFINITION pr3_gen_abst()
TYPE =
∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Bind Abst) u1 t1) x
→(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))
BODY =
assume c: C
assume u1: T
assume t1: T
assume x: T
suppose H: pr3 c (THead (Bind Abst) u1 t1) x
assume y: T
suppose H0: pr3 c y x
we proceed by induction on H0 to prove
∀x0:T
.∀x1:T
.eq T y (THead (Bind Abst) x0 x1)
→(ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t2))
case pr3_refl : t:T ⇒
the thesis becomes
∀x0:T
.∀x1:T
.∀H1:eq T t (THead (Bind Abst) x0 x1)
.ex3_2
T
T
λu2:T.λt2:T.eq T t (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t2)
assume x0: T
assume x1: T
suppose H1: eq T t (THead (Bind Abst) x0 x1)
(h1) by (pr3_refl . .) we proved pr3 c x0 x0
(h2)
assume b: B
assume u: T
by (pr3_refl . .)
we proved pr3 (CHead c (Bind b) u) x1 x1
∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 x1)
end of h2
by (ex3_2_intro . . . . . . . H1 h1 h2)
we proved
ex3_2
T
T
λu2:T.λt2:T.eq T t (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t2)
∀x0:T
.∀x1:T
.∀H1:eq T t (THead (Bind Abst) x0 x1)
.ex3_2
T
T
λu2:T.λt2:T.eq T t (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t2)
case pr3_sing : t2:T t3:T H1:pr2 c t3 t2 t4:T :pr3 c t2 t4 ⇒
the thesis becomes
∀x0:T
.∀x1:T
.∀H4:eq T t3 (THead (Bind Abst) x0 x1)
.ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t5)
(H3) by induction hypothesis we know
∀x0:T
.∀x1:T
.eq T t2 (THead (Bind Abst) x0 x1)
→(ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t5))
assume x0: T
assume x1: T
suppose H4: eq T t3 (THead (Bind Abst) x0 x1)
(H5)
we proceed by induction on H4 to prove pr2 c (THead (Bind Abst) x0 x1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
pr2 c (THead (Bind Abst) x0 x1) t2
end of H5
(H6)
by (pr2_gen_abst . . . . H5)
ex3_2
T
T
λu2:T.λt2:T.eq T t2 (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr2 c x0 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x1 t2)
end of H6
we proceed by induction on H6 to prove
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t5)
case ex3_2_intro : x2:T x3:T H7:eq T t2 (THead (Bind Abst) x2 x3) H8:pr2 c x0 x2 H9:∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x1 x3) ⇒
the thesis becomes
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t5)
(H10)
we proceed by induction on H7 to prove
∀x4:T
.∀x5:T
.eq T (THead (Bind Abst) x2 x3) (THead (Bind Abst) x4 x5)
→(ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x4 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x5 t5))
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀x4:T
.∀x5:T
.eq T (THead (Bind Abst) x2 x3) (THead (Bind Abst) x4 x5)
→(ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x4 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x5 t5))
end of H10
(H11)
by (refl_equal . .)
we proved eq T (THead (Bind Abst) x2 x3) (THead (Bind Abst) x2 x3)
by (H10 . . previous)
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x2 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x3 t5)
end of H11
we proceed by induction on H11 to prove
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t5)
case ex3_2_intro : x4:T x5:T H12:eq T t4 (THead (Bind Abst) x4 x5) H13:pr3 c x2 x4 H14:∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x3 x5) ⇒
the thesis becomes
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t5)
(h1)
by (pr3_sing . . . H8 . H13)
pr3 c x0 x4
end of h1
(h2)
assume b: B
assume u: T
(h1)
by (H9 . .)
pr2 (CHead c (Bind b) u) x1 x3
end of h1
(h2)
by (H14 . .)
pr3 (CHead c (Bind b) u) x3 x5
end of h2
by (pr3_sing . . . h1 . h2)
we proved pr3 (CHead c (Bind b) u) x1 x5
∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 x5)
end of h2
by (ex3_2_intro . . . . . . . H12 h1 h2)
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t5)
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t5)
we proved
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t5)
∀x0:T
.∀x1:T
.∀H4:eq T t3 (THead (Bind Abst) x0 x1)
.ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abst) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t5)
we proved
∀x0:T
.∀x1:T
.eq T y (THead (Bind Abst) x0 x1)
→(ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t2))
by (unintro . . . previous)
we proved
∀x0:T
.eq T y (THead (Bind Abst) u1 x0)
→(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) x0 t2))
by (unintro . . . previous)
we proved
eq T y (THead (Bind Abst) u1 t1)
→(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))
we proved
∀y:T
.pr3 c y x
→(eq T y (THead (Bind Abst) u1 t1)
→(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)))
by (insert_eq . . . . previous H)
we proved
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)
we proved
∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr3 c (THead (Bind Abst) u1 t1) x
→(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))