DEFINITION pr3_gen_abbr()
TYPE =
∀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))
BODY =
assume c: C
assume u1: T
assume t1: T
assume x: T
suppose H: pr3 c (THead (Bind Abbr) 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 Abbr) x0 x1)
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abbr) x0) x1 t2
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O x))
case pr3_refl : t:T ⇒
the thesis becomes
∀x0:T
.∀x1:T
.∀H1:eq T t (THead (Bind Abbr) x0 x1)
.or
ex3_2
T
T
λu2:T.λt2:T.eq T t (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abbr) x0) x1 t2
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t)
assume x0: T
assume x1: T
suppose H1: eq T t (THead (Bind Abbr) x0 x1)
(h1)
by (refl_equal . .)
eq T (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) x0 x1)
end of h1
(h2) by (pr3_refl . .) we proved pr3 c x0 x0
(h3)
by (pr3_refl . .)
pr3 (CHead c (Bind Abbr) x0) x1 x1
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λu2:T.λt2:T.eq T (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abbr) x0) x1 t2
by (or_introl . . previous)
we proved
or
ex3_2
T
T
λu2:T.λt2:T.eq T (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abbr) x0) x1 t2
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O (THead (Bind Abbr) x0 x1))
by (eq_ind_r . . . previous . H1)
we proved
or
ex3_2
T
T
λu2:T.λt2:T.eq T t (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abbr) x0) x1 t2
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t)
∀x0:T
.∀x1:T
.∀H1:eq T t (THead (Bind Abbr) x0 x1)
.or
ex3_2
T
T
λu2:T.λt2:T.eq T t (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abbr) x0) x1 t2
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t)
case pr3_sing : t2:T t3:T H1:pr2 c t3 t2 t4:T H2:pr3 c t2 t4 ⇒
the thesis becomes
∀x0:T
.∀x1:T
.∀H4:eq T t3 (THead (Bind Abbr) x0 x1)
.or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
(H3) by induction hypothesis we know
∀x0:T
.∀x1:T
.eq T t2 (THead (Bind Abbr) x0 x1)
→(or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4))
assume x0: T
assume x1: T
suppose H4: eq T t3 (THead (Bind Abbr) x0 x1)
(H5)
we proceed by induction on H4 to prove pr2 c (THead (Bind Abbr) x0 x1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
pr2 c (THead (Bind Abbr) x0 x1) t2
end of H5
(H6)
by (pr2_gen_abbr . . . . H5)
or
ex3_2
T
T
λu2:T.λt2:T.eq T t2 (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.pr2 c x0 u2
λ:T
.λt2:T
.or3
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x1 t2)
ex2 T λu:T.pr0 x0 u λu:T.pr2 (CHead c (Bind Abbr) u) x1 t2
ex3_2
T
T
λy:T.λ:T.pr2 (CHead c (Bind Abbr) x0) x1 y
λy:T.λz:T.pr0 y z
λ:T.λz:T.pr2 (CHead c (Bind Abbr) x0) z t2
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x1 (lift (S O) O t2))
end of H6
we proceed by induction on H6 to prove
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case or_introl : H7:ex3_2 T T λu2:T.λt5:T.eq T t2 (THead (Bind Abbr) u2 t5) λu2:T.λ:T.pr2 c x0 u2 λ:T.λt5:T.or3 ∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x1 t5) (ex2 T λu:T.pr0 x0 u λu:T.pr2 (CHead c (Bind Abbr) u) x1 t5) (ex3_2 T T λy0:T.λ:T.pr2 (CHead c (Bind Abbr) x0) x1 y0 λy0:T.λz:T.pr0 y0 z λ:T.λz:T.pr2 (CHead c (Bind Abbr) x0) z t5) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
we proceed by induction on H7 to prove
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case ex3_2_intro : x2:T x3:T H8:eq T t2 (THead (Bind Abbr) x2 x3) H9:pr2 c x0 x2 H10:or3 ∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x1 x3) (ex2 T λu:T.pr0 x0 u λu:T.pr2 (CHead c (Bind Abbr) u) x1 x3) (ex3_2 T T λy0:T.λ:T.pr2 (CHead c (Bind Abbr) x0) x1 y0 λy0:T.λz:T.pr0 y0 z λ:T.λz:T.pr2 (CHead c (Bind Abbr) x0) z x3) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
we proceed by induction on H10 to prove
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case or3_intro0 : H11:∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x1 x3) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
(H12)
we proceed by induction on H8 to prove
∀x4:T
.∀x5:T
.eq T (THead (Bind Abbr) x2 x3) (THead (Bind Abbr) x4 x5)
→(or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x4 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x4) x5 t5
pr3 (CHead c (Bind Abbr) x4) x5 (lift (S O) O t4))
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀x4:T
.∀x5:T
.eq T (THead (Bind Abbr) x2 x3) (THead (Bind Abbr) x4 x5)
→(or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x4 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x4) x5 t5
pr3 (CHead c (Bind Abbr) x4) x5 (lift (S O) O t4))
end of H12
(H13)
by (refl_equal . .)
we proved eq T (THead (Bind Abbr) x2 x3) (THead (Bind Abbr) x2 x3)
by (H12 . . previous)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x2 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x2) x3 t5
pr3 (CHead c (Bind Abbr) x2) x3 (lift (S O) O t4)
end of H13
we proceed by induction on H13 to prove
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case or_introl : H14:ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5) λu2:T.λ:T.pr3 c x2 u2 λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x2) x3 t5 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
we proceed by induction on H14 to prove
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case ex3_2_intro : x4:T x5:T H15:eq T t4 (THead (Bind Abbr) x4 x5) H16:pr3 c x2 x4 H17:pr3 (CHead c (Bind Abbr) x2) x3 x5 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
(h1)
by (refl_equal . .)
eq T (THead (Bind Abbr) x4 x5) (THead (Bind Abbr) x4 x5)
end of h1
(h2)
by (pr3_sing . . . H9 . H16)
pr3 c x0 x4
end of h2
(h3)
(h1)
by (H11 . .)
pr2 (CHead c (Bind Abbr) x0) x1 x3
end of h1
(h2)
by (pr3_pr2_pr3_t . . . . . H17 . H9)
pr3 (CHead c (Bind Abbr) x0) x3 x5
end of h2
by (pr3_sing . . . h1 . h2)
pr3 (CHead c (Bind Abbr) x0) x1 x5
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λu2:T.λt5:T.eq T (THead (Bind Abbr) x4 x5) (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
by (or_introl . . previous)
we proved
or
ex3_2
T
T
λu2:T.λt5:T.eq T (THead (Bind Abbr) x4 x5) (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O (THead (Bind Abbr) x4 x5))
by (eq_ind_r . . . previous . H15)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case or_intror : H14:pr3 (CHead c (Bind Abbr) x2) x3 (lift (S O) O t4) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
(h1)
by (H11 . .)
pr2 (CHead c (Bind Abbr) x0) x1 x3
end of h1
(h2)
by (pr3_pr2_pr3_t . . . . . H14 . H9)
pr3 (CHead c (Bind Abbr) x0) x3 (lift (S O) O t4)
end of h2
by (pr3_sing . . . h1 . h2)
we proved pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
by (or_intror . . previous)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case or3_intro1 : H11:ex2 T λu:T.pr0 x0 u λu:T.pr2 (CHead c (Bind Abbr) u) x1 x3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
we proceed by induction on H11 to prove
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case ex_intro2 : x4:T H12:pr0 x0 x4 H13:pr2 (CHead c (Bind Abbr) x4) x1 x3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
(H14)
we proceed by induction on H8 to prove
∀x5:T
.∀x6:T
.eq T (THead (Bind Abbr) x2 x3) (THead (Bind Abbr) x5 x6)
→(or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x5 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x5) x6 t5
pr3 (CHead c (Bind Abbr) x5) x6 (lift (S O) O t4))
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀x5:T
.∀x6:T
.eq T (THead (Bind Abbr) x2 x3) (THead (Bind Abbr) x5 x6)
→(or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x5 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x5) x6 t5
pr3 (CHead c (Bind Abbr) x5) x6 (lift (S O) O t4))
end of H14
(H15)
by (refl_equal . .)
we proved eq T (THead (Bind Abbr) x2 x3) (THead (Bind Abbr) x2 x3)
by (H14 . . previous)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x2 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x2) x3 t5
pr3 (CHead c (Bind Abbr) x2) x3 (lift (S O) O t4)
end of H15
we proceed by induction on H15 to prove
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case or_introl : H16:ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5) λu2:T.λ:T.pr3 c x2 u2 λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x2) x3 t5 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
we proceed by induction on H16 to prove
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case ex3_2_intro : x5:T x6:T H17:eq T t4 (THead (Bind Abbr) x5 x6) H18:pr3 c x2 x5 H19:pr3 (CHead c (Bind Abbr) x2) x3 x6 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
(h1)
by (refl_equal . .)
eq T (THead (Bind Abbr) x5 x6) (THead (Bind Abbr) x5 x6)
end of h1
(h2)
by (pr3_sing . . . H9 . H18)
pr3 c x0 x5
end of h2
(h3)
(h1)
by (pr3_pr0_pr2_t . . H12 . . . . H13)
pr3 (CHead c (Bind Abbr) x0) x1 x3
end of h1
(h2)
by (pr3_pr2_pr3_t . . . . . H19 . H9)
pr3 (CHead c (Bind Abbr) x0) x3 x6
end of h2
by (pr3_t . . . h1 . h2)
pr3 (CHead c (Bind Abbr) x0) x1 x6
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λu2:T.λt5:T.eq T (THead (Bind Abbr) x5 x6) (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
by (or_introl . . previous)
we proved
or
ex3_2
T
T
λu2:T.λt5:T.eq T (THead (Bind Abbr) x5 x6) (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O (THead (Bind Abbr) x5 x6))
by (eq_ind_r . . . previous . H17)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case or_intror : H16:pr3 (CHead c (Bind Abbr) x2) x3 (lift (S O) O t4) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
(h1)
by (pr3_pr0_pr2_t . . H12 . . . . H13)
pr3 (CHead c (Bind Abbr) x0) x1 x3
end of h1
(h2)
by (pr3_pr2_pr3_t . . . . . H16 . H9)
pr3 (CHead c (Bind Abbr) x0) x3 (lift (S O) O t4)
end of h2
by (pr3_t . . . h1 . h2)
we proved pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
by (or_intror . . previous)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case or3_intro2 : H11:ex3_2 T T λy0:T.λ:T.pr2 (CHead c (Bind Abbr) x0) x1 y0 λy0:T.λz:T.pr0 y0 z λ:T.λz:T.pr2 (CHead c (Bind Abbr) x0) z x3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
we proceed by induction on H11 to prove
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case ex3_2_intro : x4:T x5:T H12:pr2 (CHead c (Bind Abbr) x0) x1 x4 H13:pr0 x4 x5 H14:pr2 (CHead c (Bind Abbr) x0) x5 x3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
(H15)
we proceed by induction on H8 to prove
∀x6:T
.∀x7:T
.eq T (THead (Bind Abbr) x2 x3) (THead (Bind Abbr) x6 x7)
→(or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x6 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x6) x7 t5
pr3 (CHead c (Bind Abbr) x6) x7 (lift (S O) O t4))
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀x6:T
.∀x7:T
.eq T (THead (Bind Abbr) x2 x3) (THead (Bind Abbr) x6 x7)
→(or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x6 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x6) x7 t5
pr3 (CHead c (Bind Abbr) x6) x7 (lift (S O) O t4))
end of H15
(H16)
by (refl_equal . .)
we proved eq T (THead (Bind Abbr) x2 x3) (THead (Bind Abbr) x2 x3)
by (H15 . . previous)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x2 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x2) x3 t5
pr3 (CHead c (Bind Abbr) x2) x3 (lift (S O) O t4)
end of H16
we proceed by induction on H16 to prove
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case or_introl : H17:ex3_2 T T λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5) λu2:T.λ:T.pr3 c x2 u2 λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x2) x3 t5 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
we proceed by induction on H17 to prove
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case ex3_2_intro : x6:T x7:T H18:eq T t4 (THead (Bind Abbr) x6 x7) H19:pr3 c x2 x6 H20:pr3 (CHead c (Bind Abbr) x2) x3 x7 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
(h1)
by (refl_equal . .)
eq T (THead (Bind Abbr) x6 x7) (THead (Bind Abbr) x6 x7)
end of h1
(h2)
by (pr3_sing . . . H9 . H19)
pr3 c x0 x6
end of h2
(h3)
(h1)
by (pr2_free . . . H13)
pr2 (CHead c (Bind Abbr) x0) x4 x5
end of h1
(h2)
by (pr3_pr2_pr3_t . . . . . H20 . H9)
we proved pr3 (CHead c (Bind Abbr) x0) x3 x7
by (pr3_sing . . . H14 . previous)
pr3 (CHead c (Bind Abbr) x0) x5 x7
end of h2
by (pr3_sing . . . h1 . h2)
we proved pr3 (CHead c (Bind Abbr) x0) x4 x7
by (pr3_sing . . . H12 . previous)
pr3 (CHead c (Bind Abbr) x0) x1 x7
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λu2:T.λt5:T.eq T (THead (Bind Abbr) x6 x7) (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
by (or_introl . . previous)
we proved
or
ex3_2
T
T
λu2:T.λt5:T.eq T (THead (Bind Abbr) x6 x7) (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O (THead (Bind Abbr) x6 x7))
by (eq_ind_r . . . previous . H18)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case or_intror : H17:pr3 (CHead c (Bind Abbr) x2) x3 (lift (S O) O t4) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
(h1)
by (pr2_free . . . H13)
pr2 (CHead c (Bind Abbr) x0) x4 x5
end of h1
(h2)
by (pr3_pr2_pr3_t . . . . . H17 . H9)
we proved pr3 (CHead c (Bind Abbr) x0) x3 (lift (S O) O t4)
by (pr3_sing . . . H14 . previous)
pr3 (CHead c (Bind Abbr) x0) x5 (lift (S O) O t4)
end of h2
by (pr3_sing . . . h1 . h2)
we proved pr3 (CHead c (Bind Abbr) x0) x4 (lift (S O) O t4)
by (pr3_sing . . . H12 . previous)
we proved pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
by (or_intror . . previous)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
case or_intror : H7:∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x1 (lift (S O) O t2)) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
(h1)
by (H7 . .)
pr2 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t2)
end of h1
(h2)
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 .)
we proved drop (S O) O (CHead c (Bind Abbr) x0) c
by (pr3_lift . . . . previous . . H2)
pr3 (CHead c (Bind Abbr) x0) (lift (S O) O t2) (lift (S O) O t4)
end of h2
by (pr3_sing . . . h1 . h2)
we proved pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
by (or_intror . . previous)
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
we proved
or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
∀x0:T
.∀x1:T
.∀H4:eq T t3 (THead (Bind Abbr) x0 x1)
.or
ex3_2
T
T
λu2:T.λt5:T.eq T t4 (THead (Bind Abbr) u2 t5)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt5:T.pr3 (CHead c (Bind Abbr) x0) x1 t5
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)
we proved
∀x0:T
.∀x1:T
.eq T y (THead (Bind Abbr) x0 x1)
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.pr3 (CHead c (Bind Abbr) x0) x1 t2
pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O x))
by (unintro . . . previous)
we proved
∀x0:T
.eq T y (THead (Bind Abbr) u1 x0)
→(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) x0 t2
pr3 (CHead c (Bind Abbr) u1) x0 (lift (S O) O x))
by (unintro . . . previous)
we proved
eq T y (THead (Bind Abbr) u1 t1)
→(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
∀y:T
.pr3 c y x
→(eq T y (THead (Bind Abbr) u1 t1)
→(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 (insert_eq . . . . previous H)
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)
we proved
∀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))