DEFINITION pr2_gen_abbr()
TYPE =
∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr2 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.pr2 c u1 u2
λ:T
.λt2:T
.or3
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c (Bind Abbr) u) t1 t2
ex3_2
T
T
λy:T.λ:T.pr2 (CHead c (Bind Abbr) u1) t1 y
λy:T.λz:T.pr0 y z
λ:T.λz:T.pr2 (CHead c (Bind Abbr) u1) z t2
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 (lift (S O) O x)))
BODY =
assume c: C
assume u1: T
assume t1: T
assume x: T
suppose H: pr2 c (THead (Bind Abbr) 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 Abbr) u1 t1)
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.pr2 c u1 u2
λ:T
.λt2:T
.or3
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c (Bind Abbr) u) t1 t2
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c (Bind Abbr) u1) z t2
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 (lift (S O) O x)))
case pr2_free : c0:C t0:T t2:T H1:pr0 t0 t2 ⇒
the thesis becomes
∀H2:eq T t0 (THead (Bind Abbr) u1 t1)
.or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
suppose H2: eq T t0 (THead (Bind Abbr) u1 t1)
(H3)
we proceed by induction on H2 to prove pr0 (THead (Bind Abbr) u1 t1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
pr0 (THead (Bind Abbr) u1 t1) t2
end of H3
by (pr0_gen_abbr . . . H3)
we proved
or
ex3_2
T
T
λu2:T.λt2:T.eq T t2 (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.pr0 u1 u2
λu2:T.λt2:T.or (pr0 t1 t2) (ex2 T λy:T.pr0 t1 y λy:T.subst0 O u2 y t2)
pr0 t1 (lift (S O) O t2)
we proceed by induction on the previous result to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
case or_introl : H4:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3) λu2:T.λ:T.pr0 u1 u2 λu2:T.λt3:T.or (pr0 t1 t3) (ex2 T λy0:T.pr0 t1 y0 λy0:T.subst0 O u2 y0 t3) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
we proceed by induction on H4 to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
case ex3_2_intro : x0:T x1:T H5:eq T t2 (THead (Bind Abbr) x0 x1) H6:pr0 u1 x0 H_x:or (pr0 t1 x1) (ex2 T λy0:T.pr0 t1 y0 λy0:T.subst0 O x0 y0 x1) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
we proceed by induction on H_x to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
case or_introl : H7:pr0 t1 x1 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
(h1)
by (refl_equal . .)
eq T (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) x0 x1)
end of h1
(h2) by (pr2_free . . . H6) we proved pr2 c0 u1 x0
(h3)
assume b: B
assume u: T
by (pr2_free . . . H7)
we proved pr2 (CHead c0 (Bind b) u) t1 x1
we proved ∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 x1)
by (or3_intro0 . . . previous)
or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 x1)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 x1
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z 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 Abbr) x0 x1) (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
by (or_introl . . previous)
we proved
or
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B
.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O (THead (Bind Abbr) x0 x1)))
by (eq_ind_r . . . previous . H5)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
case or_intror : H_x0:ex2 T λy0:T.pr0 t1 y0 λy0:T.subst0 O x0 y0 x1 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
we proceed by induction on H_x0 to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
case ex_intro2 : x2:T H7:pr0 t1 x2 H8:subst0 O x0 x2 x1 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
by (pr0_subst0_back . . . . H8 . H6)
we proved ex2 T λt:T.subst0 O u1 x2 t λt:T.pr0 t x1
we proceed by induction on the previous result to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B
.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O (THead (Bind Abbr) x0 x1)))
case ex_intro2 : x3:T :subst0 O u1 x2 x3 :pr0 x3 x1 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B
.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O (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 (pr2_free . . . H6) we proved pr2 c0 u1 x0
(h3)
by (getl_refl . . .)
we proved getl O (CHead c0 (Bind Abbr) x0) (CHead c0 (Bind Abbr) x0)
by (pr2_delta . . . . previous . . H7 . H8)
we proved pr2 (CHead c0 (Bind Abbr) x0) t1 x1
by (ex_intro2 . . . . H6 previous)
we proved ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 x1
by (or3_intro1 . . . previous)
or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 x1)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 x1
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z 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 Abbr) x0 x1) (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
by (or_introl . . previous)
or
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B
.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O (THead (Bind Abbr) x0 x1)))
we proved
or
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B
.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O (THead (Bind Abbr) x0 x1)))
by (eq_ind_r . . . previous . H5)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
case or_intror : H4:pr0 t1 (lift (S O) O t2) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
assume b: B
assume u: T
by (pr2_free . . . H4)
we proved pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2)
we proved ∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
by (or_intror . . previous)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
we proved
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
∀H2:eq T t0 (THead (Bind Abbr) u1 t1)
.or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c0 (Bind Abbr) u) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
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 Abbr) u1 t1)
.or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
suppose H4: eq T t0 (THead (Bind Abbr) u1 t1)
(H5)
we proceed by induction on H4 to prove pr0 (THead (Bind Abbr) u1 t1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
pr0 (THead (Bind Abbr) u1 t1) t2
end of H5
by (pr0_gen_abbr . . . H5)
we proved
or
ex3_2
T
T
λu2:T.λt2:T.eq T t2 (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.pr0 u1 u2
λu2:T.λt2:T.or (pr0 t1 t2) (ex2 T λy:T.pr0 t1 y λy:T.subst0 O u2 y t2)
pr0 t1 (lift (S O) O t2)
we proceed by induction on the previous result to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case or_introl : H6:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3) λu2:T.λ:T.pr0 u1 u2 λu2:T.λt3:T.or (pr0 t1 t3) (ex2 T λy0:T.pr0 t1 y0 λy0:T.subst0 O u2 y0 t3) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
we proceed by induction on H6 to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case ex3_2_intro : x0:T x1:T H7:eq T t2 (THead (Bind Abbr) x0 x1) H8:pr0 u1 x0 H_x:or (pr0 t1 x1) (ex2 T λy0:T.pr0 t1 y0 λy0:T.subst0 O x0 y0 x1) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
we proceed by induction on H_x to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case or_introl : H9:pr0 t1 x1 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
(H10)
we proceed by induction on H7 to prove subst0 i u (THead (Bind Abbr) x0 x1) t
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 i u (THead (Bind Abbr) x0 x1) t
end of H10
by (subst0_gen_head . . . . . . H10)
we proved
or3
ex2 T λu2:T.eq T t (THead (Bind Abbr) u2 x1) λu2:T.subst0 i u x0 u2
ex2 T λt2:T.eq T t (THead (Bind Abbr) x0 t2) λt2:T.subst0 (s (Bind Abbr) i) u x1 t2
ex3_2
T
T
λu2:T.λt2:T.eq T t (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.subst0 i u x0 u2
λ:T.λt2:T.subst0 (s (Bind Abbr) i) u x1 t2
we proceed by induction on the previous result to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case or3_intro0 : H11:ex2 T λu2:T.eq T t (THead (Bind Abbr) u2 x1) λu2:T.subst0 i u x0 u2 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
we proceed by induction on H11 to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case ex_intro2 : x2:T H12:eq T t (THead (Bind Abbr) x2 x1) H13:subst0 i u x0 x2 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
(h1)
by (pr2_delta . . . . H1 . . H8 . H13)
pr2 c0 u1 x2
end of h1
(h2)
assume b: B
assume u0: T
by (pr2_free . . . H9)
we proved pr2 (CHead c0 (Bind b) u0) t1 x1
we proved ∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 x1)
by (or3_intro0 . . . previous)
or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 x1)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 x1
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z x1
end of h2
by (ex3_2_intro . . . . . . . H12 h1 h2)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
by (or_introl . . previous)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case or3_intro1 : H11:ex2 T λt3:T.eq T t (THead (Bind Abbr) x0 t3) λt3:T.subst0 (s (Bind Abbr) i) u x1 t3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
we proceed by induction on H11 to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case ex_intro2 : x2:T H12:eq T t (THead (Bind Abbr) x0 x2) H13:subst0 (s (Bind Abbr) i) u x1 x2 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
(h1) by (pr2_free . . . H8) we proved pr2 c0 u1 x0
(h2)
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 Abbr) i) u x1 x2
subst0 (S i) u x1 x2
end of h2
by (pr2_delta . . . . h1 . . H9 . h2)
we proved pr2 (CHead c0 (Bind b) u0) t1 x2
we proved ∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 x2)
by (or3_intro0 . . . previous)
or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 x2)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 x2
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z x2
end of h2
by (ex3_2_intro . . . . . . . H12 h1 h2)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
by (or_introl . . previous)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case or3_intro2 : H11:ex3_2 T T λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3) λu2:T.λ:T.subst0 i u x0 u2 λ:T.λt3:T.subst0 (s (Bind Abbr) i) u x1 t3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
we proceed by induction on H11 to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case ex3_2_intro : x2:T x3:T H12:eq T t (THead (Bind Abbr) x2 x3) H13:subst0 i u x0 x2 H14:subst0 (s (Bind Abbr) i) u x1 x3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
(h1)
by (pr2_delta . . . . H1 . . H8 . H13)
pr2 c0 u1 x2
end of h1
(h2)
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 H14
we proved subst0 (s (Bind Abbr) i) u x1 x3
subst0 (S i) u x1 x3
end of h2
by (pr2_delta . . . . h1 . . H9 . h2)
we proved pr2 (CHead c0 (Bind b) u0) t1 x3
we proved ∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 x3)
by (or3_intro0 . . . previous)
or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 x3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 x3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z x3
end of h2
by (ex3_2_intro . . . . . . . H12 h1 h2)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
by (or_introl . . previous)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case or_intror : H_x0:ex2 T λy0:T.pr0 t1 y0 λy0:T.subst0 O x0 y0 x1 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
we proceed by induction on H_x0 to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case ex_intro2 : x2:T H9:pr0 t1 x2 H10:subst0 O x0 x2 x1 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
(H11)
we proceed by induction on H7 to prove subst0 i u (THead (Bind Abbr) x0 x1) t
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 i u (THead (Bind Abbr) x0 x1) t
end of H11
by (subst0_gen_head . . . . . . H11)
we proved
or3
ex2 T λu2:T.eq T t (THead (Bind Abbr) u2 x1) λu2:T.subst0 i u x0 u2
ex2 T λt2:T.eq T t (THead (Bind Abbr) x0 t2) λt2:T.subst0 (s (Bind Abbr) i) u x1 t2
ex3_2
T
T
λu2:T.λt2:T.eq T t (THead (Bind Abbr) u2 t2)
λu2:T.λ:T.subst0 i u x0 u2
λ:T.λt2:T.subst0 (s (Bind Abbr) i) u x1 t2
we proceed by induction on the previous result to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case or3_intro0 : H12:ex2 T λu2:T.eq T t (THead (Bind Abbr) u2 x1) λu2:T.subst0 i u x0 u2 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
we proceed by induction on H12 to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case ex_intro2 : x3:T H13:eq T t (THead (Bind Abbr) x3 x1) H14:subst0 i u x0 x3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
by (pr0_subst0_back . . . . H10 . H8)
we proved ex2 T λt:T.subst0 O u1 x2 t λt:T.pr0 t x1
we proceed by induction on the previous result to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case ex_intro2 : x4:T :subst0 O u1 x2 x4 :pr0 x4 x1 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
(h1)
by (pr2_delta . . . . H1 . . H8 . H14)
pr2 c0 u1 x3
end of h1
(h2)
by (getl_refl . . .)
we proved getl O (CHead c0 (Bind Abbr) x0) (CHead c0 (Bind Abbr) x0)
by (pr2_delta . . . . previous . . H9 . H10)
we proved pr2 (CHead c0 (Bind Abbr) x0) t1 x1
by (ex_intro2 . . . . H8 previous)
we proved ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 x1
by (or3_intro1 . . . previous)
or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 x1)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 x1
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z x1
end of h2
by (ex3_2_intro . . . . . . . H13 h1 h2)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
by (or_introl . . previous)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case or3_intro1 : H12:ex2 T λt3:T.eq T t (THead (Bind Abbr) x0 t3) λt3:T.subst0 (s (Bind Abbr) i) u x1 t3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
we proceed by induction on H12 to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case ex_intro2 : x3:T H13:eq T t (THead (Bind Abbr) x0 x3) H14:subst0 (s (Bind Abbr) i) u x1 x3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
by (pr0_subst0_back . . . . H10 . H8)
we proved ex2 T λt:T.subst0 O u1 x2 t λt:T.pr0 t x1
we proceed by induction on the previous result to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case ex_intro2 : x4:T H15:subst0 O u1 x2 x4 H16:pr0 x4 x1 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
(h1) by (pr2_free . . . H8) we proved pr2 c0 u1 x0
(h2)
(h1)
by (getl_refl . . .)
we proved getl O (CHead c0 (Bind Abbr) u1) (CHead c0 (Bind Abbr) u1)
by (pr2_delta . . . . previous . . H9 . H15)
pr2 (CHead c0 (Bind Abbr) u1) t1 x4
end of h1
(h2)
(h1)
consider H1
we proved getl i c0 (CHead d (Bind Abbr) u)
that is equivalent to getl (r (Bind Abbr) i) c0 (CHead d (Bind Abbr) u)
by (getl_head . . . . previous .)
getl (S i) (CHead c0 (Bind Abbr) u1) (CHead d (Bind Abbr) u)
end of h1
(h2) by (pr0_refl .) we proved pr0 x1 x1
(h3)
consider H14
we proved subst0 (s (Bind Abbr) i) u x1 x3
subst0 (S i) u x1 x3
end of h3
by (pr2_delta . . . . h1 . . h2 . h3)
pr2 (CHead c0 (Bind Abbr) u1) x1 x3
end of h2
by (ex3_2_intro . . . . . . . h1 H16 h2)
we proved
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z x3
by (or3_intro2 . . . previous)
or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 x3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 x3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z x3
end of h2
by (ex3_2_intro . . . . . . . H13 h1 h2)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
by (or_introl . . previous)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case or3_intro2 : H12:ex3_2 T T λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3) λu2:T.λ:T.subst0 i u x0 u2 λ:T.λt3:T.subst0 (s (Bind Abbr) i) u x1 t3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
we proceed by induction on H12 to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case ex3_2_intro : x3:T x4:T H13:eq T t (THead (Bind Abbr) x3 x4) H14:subst0 i u x0 x3 H15:subst0 (s (Bind Abbr) i) u x1 x4 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
by (pr0_subst0_back . . . . H10 . H8)
we proved ex2 T λt:T.subst0 O u1 x2 t λt:T.pr0 t x1
we proceed by induction on the previous result to prove
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case ex_intro2 : x5:T H16:subst0 O u1 x2 x5 H17:pr0 x5 x1 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
(h1)
by (pr2_delta . . . . H1 . . H8 . H14)
pr2 c0 u1 x3
end of h1
(h2)
(h1)
by (getl_refl . . .)
we proved getl O (CHead c0 (Bind Abbr) u1) (CHead c0 (Bind Abbr) u1)
by (pr2_delta . . . . previous . . H9 . H16)
pr2 (CHead c0 (Bind Abbr) u1) t1 x5
end of h1
(h2)
(h1)
consider H1
we proved getl i c0 (CHead d (Bind Abbr) u)
that is equivalent to getl (r (Bind Abbr) i) c0 (CHead d (Bind Abbr) u)
by (getl_head . . . . previous .)
getl (S i) (CHead c0 (Bind Abbr) u1) (CHead d (Bind Abbr) u)
end of h1
(h2) by (pr0_refl .) we proved pr0 x1 x1
(h3)
consider H15
we proved subst0 (s (Bind Abbr) i) u x1 x4
subst0 (S i) u x1 x4
end of h3
by (pr2_delta . . . . h1 . . h2 . h3)
pr2 (CHead c0 (Bind Abbr) u1) x1 x4
end of h2
by (ex3_2_intro . . . . . . . h1 H17 h2)
we proved
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z x4
by (or3_intro2 . . . previous)
or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 x4)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 x4
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z x4
end of h2
by (ex3_2_intro . . . . . . . H13 h1 h2)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
by (or_introl . . previous)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
case or_intror : H6:pr0 t1 (lift (S O) O t2) ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
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)
by (le_O_n .)
we proved le O i
by (subst0_lift_ge_S . . . . H3 . previous)
subst0 (S i) u (lift (S O) O t2) (lift (S O) O t)
end of h2
by (pr2_delta . . . . h1 . . H6 . h2)
we proved pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t)
we proved ∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
by (or_intror . . previous)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
we proved
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
∀H4:eq T t0 (THead (Bind Abbr) u1 t1)
.or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Abbr) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T
.λt3:T
.or3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
ex2 T λu0:T.pr0 u1 u0 λu0:T.pr2 (CHead c0 (Bind Abbr) u0) t1 t3
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c0 (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c0 (Bind Abbr) u1) z t3
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
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.pr2 c u1 u2
λ:T
.λt2:T
.or3
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c (Bind Abbr) u) t1 t2
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c (Bind Abbr) u1) z t2
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 (lift (S O) O x)))
we proved
∀y:T
.pr2 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.pr2 c u1 u2
λ:T
.λt2:T
.or3
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c (Bind Abbr) u) t1 t2
ex3_2
T
T
λy0:T.λ:T.pr2 (CHead c (Bind Abbr) u1) t1 y0
λy0:T.λz:T.pr0 y0 z
λ:T.λz:T.pr2 (CHead c (Bind Abbr) u1) z t2
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) 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.pr2 c u1 u2
λ:T
.λt2:T
.or3
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c (Bind Abbr) u) t1 t2
ex3_2
T
T
λy:T.λ:T.pr2 (CHead c (Bind Abbr) u1) t1 y
λy:T.λz:T.pr0 y z
λ:T.λz:T.pr2 (CHead c (Bind Abbr) u1) z t2
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 (lift (S O) O x))
we proved
∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr2 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.pr2 c u1 u2
λ:T
.λt2:T
.or3
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2)
ex2 T λu:T.pr0 u1 u λu:T.pr2 (CHead c (Bind Abbr) u) t1 t2
ex3_2
T
T
λy:T.λ:T.pr2 (CHead c (Bind Abbr) u1) t1 y
λy:T.λz:T.pr0 y z
λ:T.λz:T.pr2 (CHead c (Bind Abbr) u1) z t2
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 (lift (S O) O x)))