DEFINITION pr2_gen_void()
TYPE =
∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr2 c (THead (Bind Void) u1 t1) x
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Void) u2 t2)
λu2:T.λ:T.pr2 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 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 Void) 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 Void) u1 t1)
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Void) u2 t2)
λu2:T.λ:T.pr2 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 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 Void) u1 t1)
.or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
suppose H2: eq T t0 (THead (Bind Void) u1 t1)
(H3)
we proceed by induction on H2 to prove pr0 (THead (Bind Void) u1 t1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
pr0 (THead (Bind Void) u1 t1) t2
end of H3
by (pr0_gen_void . . . H3)
we proved
or
ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Bind Void) u2 t2) λu2:T.λ:T.pr0 u1 u2 λ:T.λt2:T.pr0 t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 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 Void) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 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 Void) x0 x1) H6:pr0 u1 x0 H7:pr0 t1 x1 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 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 Void) x0 x1) (THead (Bind Void) 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
∀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 Void) x0 x1) (THead (Bind Void) 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 (or_introl . . previous)
we proved
or
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Bind Void) x0 x1) (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
∀b:B
.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O (THead (Bind Void) x0 x1)))
by (eq_ind_r . . . previous . H5)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 t3)
∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))
∀H2:eq T t0 (THead (Bind Void) u1 t1)
.or
ex3_2
T
T
λu2:T.λt3:T.eq T t2 (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c0 (Bind b) u) t1 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 Void) u1 t1)
.or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
suppose H4: eq T t0 (THead (Bind Void) u1 t1)
(H5)
we proceed by induction on H4 to prove pr0 (THead (Bind Void) u1 t1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
pr0 (THead (Bind Void) u1 t1) t2
end of H5
by (pr0_gen_void . . . H5)
we proved
or
ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Bind Void) u2 t2) λu2:T.λ:T.pr0 u1 u2 λ:T.λt2:T.pr0 t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3) λu2:T.λ:T.pr0 u1 u2 λ:T.λt3:T.pr0 t1 t3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) x0 x1) H8:pr0 u1 x0 H9:pr0 t1 x1 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) x0 x1) t
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 i u (THead (Bind Void) x0 x1) t
end of H10
by (subst0_gen_head . . . . . . H10)
we proved
or3
ex2 T λu2:T.eq T t (THead (Bind Void) u2 x1) λu2:T.subst0 i u x0 u2
ex2 T λt2:T.eq T t (THead (Bind Void) x0 t2) λt2:T.subst0 (s (Bind Void) i) u x1 t2
ex3_2
T
T
λu2:T.λt2:T.eq T t (THead (Bind Void) u2 t2)
λu2:T.λ:T.subst0 i u x0 u2
λ:T.λt2:T.subst0 (s (Bind Void) 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) 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 (or_introl . . previous)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) x0 t3) λt3:T.subst0 (s (Bind Void) i) u x1 t3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) x0 x2) H13:subst0 (s (Bind Void) i) u x1 x2 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) 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
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) 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 (or_introl . . previous)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3) λu2:T.λ:T.subst0 i u x0 u2 λ:T.λt3:T.subst0 (s (Bind Void) i) u x1 t3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) x2 x3) H13:subst0 i u x0 x2 H14:subst0 (s (Bind Void) i) u x1 x3 ⇒
the thesis becomes
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) 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
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) 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 (or_introl . . previous)
or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 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 Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
∀H4:eq T t0 (THead (Bind Void) u1 t1)
.or
ex3_2
T
T
λu2:T.λt3:T.eq T t (THead (Bind Void) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 t3)
∀b:B.∀u0:T.(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))
we proved
eq T y (THead (Bind Void) u1 t1)
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Void) u2 t2)
λu2:T.λ:T.pr2 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 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 Void) u1 t1)
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Void) u2 t2)
λu2:T.λ:T.pr2 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 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 Void) u2 t2)
λu2:T.λ:T.pr2 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 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 Void) u1 t1) x
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Void) u2 t2)
λu2:T.λ:T.pr2 c u1 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 t2)
∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t1 (lift (S O) O x)))