DEFINITION pr2_gen_abst()
TYPE =
∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr2 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.pr2 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2))
BODY =
assume c: C
assume u1: T
assume t1: T
assume x: T
suppose H: pr2 c (THead (Bind Abst) u1 t1) x
assume y: T
suppose H0: pr2 c y x
we proceed by induction on H0 to prove
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.pr2 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2))
case pr2_free : c0:C t0:T t2:T H1:pr0 t0 t2 ⇒
the thesis becomes
∀H2:eq T t0 (THead (Bind Abst) u1 t1)
.ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
suppose H2: eq T t0 (THead (Bind Abst) u1 t1)
(H3)
we proceed by induction on H2 to prove pr0 (THead (Bind Abst) u1 t1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
pr0 (THead (Bind Abst) u1 t1) t2
end of H3
by (pr0_gen_abst . . . H3)
we proved ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Bind Abst) u2 t2) λu2:T.λ:T.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
we proceed by induction on the previous result to prove
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
case ex3_2_intro : x0:T x1:T H4:eq T t2 (THead (Bind Abst) x0 x1) H5:pr0 u1 x0 H6:pr0 t1 x1 ⇒
the thesis becomes
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
(h1)
by (refl_equal . .)
eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) x0 x1)
end of h1
(h2) by (pr2_free . . . H5) we proved pr2 c0 u1 x0
(h3)
assume b: B
assume u: T
by (pr2_free . . . H6)
we proved pr2 (CHead c0 (Bind b) u) t1 x1
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 x1)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
by (eq_ind_r . . . previous . H4)
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
∀H2:eq T t0 (THead (Bind Abst) u1 t1)
.ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
case pr2_delta : c0:C d:C u:T i:nat H1:getl i c0 (CHead d (Bind Abbr) u) t0:T t2:T H2:pr0 t0 t2 t:T H3:subst0 i u t2 t ⇒
the thesis becomes
∀H4:eq T t0 (THead (Bind Abst) u1 t1)
.ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
suppose H4: eq T t0 (THead (Bind Abst) u1 t1)
(H5)
we proceed by induction on H4 to prove pr0 (THead (Bind Abst) u1 t1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
pr0 (THead (Bind Abst) u1 t1) t2
end of H5
by (pr0_gen_abst . . . H5)
we proved ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Bind Abst) u2 t2) λu2:T.λ:T.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2
we proceed by induction on the previous result to prove
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
case ex3_2_intro : x0:T x1:T H6:eq T t2 (THead (Bind Abst) x0 x1) H7:pr0 u1 x0 H8:pr0 t1 x1 ⇒
the thesis becomes
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
(H9)
we proceed by induction on H6 to prove subst0 i u (THead (Bind Abst) x0 x1) t
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 i u (THead (Bind Abst) x0 x1) t
end of H9
by (subst0_gen_head . . . . . . H9)
we proved
or3
ex2 T λu2:T.eq T t (THead (Bind Abst) u2 x1) λu2:T.subst0 i u x0 u2
ex2 T λt2:T.eq T t (THead (Bind Abst) x0 t2) λt2:T.subst0 (s (Bind Abst) i) u x1 t2
ex3_2
T
T
λu2:T.λt2:T.eq T t (THead (Bind Abst) u2 t2)
λu2:T.λ:T.subst0 i u x0 u2
λ:T.λt2:T.subst0 (s (Bind Abst) i) u x1 t2
we proceed by induction on the previous result to prove
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
case or3_intro0 : H10:ex2 T λu2:T.eq T t (THead (Bind Abst) u2 x1) λu2:T.subst0 i u x0 u2 ⇒
the thesis becomes
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
we proceed by induction on H10 to prove
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
case ex_intro2 : x2:T H11:eq T t (THead (Bind Abst) x2 x1) H12:subst0 i u x0 x2 ⇒
the thesis becomes
ex3_2
T
T
λu2:T.λt4:T.eq T t (THead (Bind Abst) u2 t4)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt4:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t4)
(h1)
by (refl_equal . .)
eq T (THead (Bind Abst) x2 x1) (THead (Bind Abst) x2 x1)
end of h1
(h2)
by (pr2_delta . . . . H1 . . H7 . H12)
pr2 c0 u1 x2
end of h2
(h3)
assume b: B
assume u0: T
by (pr2_free . . . H8)
we proved pr2 (CHead c0 (Bind b) u0) t1 x1
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 x1)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abst) x2 x1) (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
by (eq_ind_r . . . previous . H11)
ex3_2
T
T
λu2:T.λt4:T.eq T t (THead (Bind Abst) u2 t4)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt4:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t4)
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
case or3_intro1 : H10:ex2 T λt3:T.eq T t (THead (Bind Abst) x0 t3) λt3:T.subst0 (s (Bind Abst) i) u x1 t3 ⇒
the thesis becomes
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
we proceed by induction on H10 to prove
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
case ex_intro2 : x2:T H11:eq T t (THead (Bind Abst) x0 x2) H12:subst0 (s (Bind Abst) i) u x1 x2 ⇒
the thesis becomes
ex3_2
T
T
λu2:T.λt4:T.eq T t (THead (Bind Abst) u2 t4)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt4:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t4)
(h1)
by (refl_equal . .)
eq T (THead (Bind Abst) x0 x2) (THead (Bind Abst) x0 x2)
end of h1
(h2) by (pr2_free . . . H7) we proved pr2 c0 u1 x0
(h3)
assume b: B
assume u0: T
(h1)
consider H1
we proved getl i c0 (CHead d (Bind Abbr) u)
that is equivalent to getl (r (Bind b) i) c0 (CHead d (Bind Abbr) u)
by (getl_head . . . . previous .)
getl (S i) (CHead c0 (Bind b) u0) (CHead d (Bind Abbr) u)
end of h1
(h2)
consider H12
we proved subst0 (s (Bind Abst) i) u x1 x2
subst0 (S i) u x1 x2
end of h2
by (pr2_delta . . . . h1 . . H8 . h2)
we proved pr2 (CHead c0 (Bind b) u0) t1 x2
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 x2)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abst) x0 x2) (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
by (eq_ind_r . . . previous . H11)
ex3_2
T
T
λu2:T.λt4:T.eq T t (THead (Bind Abst) u2 t4)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt4:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t4)
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
case or3_intro2 : H10:ex3_2 T T λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3) λu2:T.λ:T.subst0 i u x0 u2 λ:T.λt3:T.subst0 (s (Bind Abst) i) u x1 t3 ⇒
the thesis becomes
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
we proceed by induction on H10 to prove
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
case ex3_2_intro : x2:T x3:T H11:eq T t (THead (Bind Abst) x2 x3) H12:subst0 i u x0 x2 H13:subst0 (s (Bind Abst) i) u x1 x3 ⇒
the thesis becomes
ex3_2
T
T
λu2:T.λt4:T.eq T t (THead (Bind Abst) u2 t4)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt4:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t4)
(h1)
by (refl_equal . .)
eq T (THead (Bind Abst) x2 x3) (THead (Bind Abst) x2 x3)
end of h1
(h2)
by (pr2_delta . . . . H1 . . H7 . H12)
pr2 c0 u1 x2
end of h2
(h3)
assume b: B
assume u0: T
(h1)
consider H1
we proved getl i c0 (CHead d (Bind Abbr) u)
that is equivalent to getl (r (Bind b) i) c0 (CHead d (Bind Abbr) u)
by (getl_head . . . . previous .)
getl (S i) (CHead c0 (Bind b) u0) (CHead d (Bind Abbr) u)
end of h1
(h2)
consider H13
we proved subst0 (s (Bind Abst) i) u x1 x3
subst0 (S i) u x1 x3
end of h2
by (pr2_delta . . . . h1 . . H8 . h2)
we proved pr2 (CHead c0 (Bind b) u0) t1 x3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 x3)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abst) x2 x3) (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
by (eq_ind_r . . . previous . H11)
ex3_2
T
T
λu2:T.λt4:T.eq T t (THead (Bind Abst) u2 t4)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt4:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t4)
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
∀H4:eq T t0 (THead (Bind Abst) u1 t1)
.ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abst) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
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.pr2 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2))
we proved
∀y:T
.pr2 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.pr2 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (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.pr2 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2)
we proved
∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr2 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.pr2 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2))