DEFINITION pr2_gen_cast()
TYPE =
∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr2 c (THead (Flat Cast) u1 t1) x
→or (ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Cast) u2 t2) λu2:T.λ:T.pr2 c u1 u2 λ:T.λt2:T.pr2 c t1 t2) (pr2 c t1 x)
BODY =
assume c: C
assume u1: T
assume t1: T
assume x: T
suppose H: pr2 c (THead (Flat Cast) u1 t1) x
assume y: T
suppose H0: pr2 c y x
we proceed by induction on H0 to prove
eq T y (THead (Flat Cast) u1 t1)
→or (ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Cast) u2 t2) λu2:T.λ:T.pr2 c u1 u2 λ:T.λt2:T.pr2 c t1 t2) (pr2 c t1 x)
case pr2_free : c0:C t0:T t2:T H1:pr0 t0 t2 ⇒
the thesis becomes
∀H2:eq T t0 (THead (Flat Cast) u1 t1)
.or (ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t2)
suppose H2: eq T t0 (THead (Flat Cast) u1 t1)
(H3)
we proceed by induction on H2 to prove pr0 (THead (Flat Cast) u1 t1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
pr0 (THead (Flat Cast) u1 t1) t2
end of H3
by (pr0_gen_cast . . . H3)
we proved or (ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Flat Cast) u2 t2) λu2:T.λ:T.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2) (pr0 t1 t2)
we proceed by induction on the previous result to prove or (ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t2)
case or_introl : H4:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) 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 (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t2)
we proceed by induction on H4 to prove or (ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t2)
case ex3_2_intro : x0:T x1:T H5:eq T t2 (THead (Flat Cast) 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 (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t2)
(h1)
by (refl_equal . .)
eq T (THead (Flat Cast) x0 x1) (THead (Flat Cast) x0 x1)
end of h1
(h2) by (pr2_free . . . H6) we proved pr2 c0 u1 x0
(h3) by (pr2_free . . . H7) we proved pr2 c0 t1 x1
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Flat Cast) x0 x1) (THead (Flat Cast) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.pr2 c0 t1 t3
by (or_introl . . previous)
we proved
or
ex3_2
T
T
λu2:T.λt3:T.eq T (THead (Flat Cast) x0 x1) (THead (Flat Cast) u2 t3)
λu2:T.λ:T.pr2 c0 u1 u2
λ:T.λt3:T.pr2 c0 t1 t3
pr2 c0 t1 (THead (Flat Cast) x0 x1)
by (eq_ind_r . . . previous . H5)
or (ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t2)
or (ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t2)
case or_intror : H4:pr0 t1 t2 ⇒
the thesis becomes or (ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t2)
by (pr2_free . . . H4)
we proved pr2 c0 t1 t2
by (or_intror . . previous)
or (ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t2)
we proved or (ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t2)
∀H2:eq T t0 (THead (Flat Cast) u1 t1)
.or (ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 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 (Flat Cast) u1 t1)
.or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
suppose H4: eq T t0 (THead (Flat Cast) u1 t1)
(H5)
we proceed by induction on H4 to prove pr0 (THead (Flat Cast) u1 t1) t2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
pr0 (THead (Flat Cast) u1 t1) t2
end of H5
by (pr0_gen_cast . . . H5)
we proved or (ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Flat Cast) u2 t2) λu2:T.λ:T.pr0 u1 u2 λ:T.λt2:T.pr0 t1 t2) (pr0 t1 t2)
we proceed by induction on the previous result to prove or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
case or_introl : H6:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) 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 (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
we proceed by induction on H6 to prove or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
case ex3_2_intro : x0:T x1:T H7:eq T t2 (THead (Flat Cast) 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 (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
(H10)
we proceed by induction on H7 to prove subst0 i u (THead (Flat Cast) x0 x1) t
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 i u (THead (Flat Cast) x0 x1) t
end of H10
by (subst0_gen_head . . . . . . H10)
we proved
or3
ex2 T λu2:T.eq T t (THead (Flat Cast) u2 x1) λu2:T.subst0 i u x0 u2
ex2 T λt2:T.eq T t (THead (Flat Cast) x0 t2) λt2:T.subst0 (s (Flat Cast) i) u x1 t2
ex3_2
T
T
λu2:T.λt2:T.eq T t (THead (Flat Cast) u2 t2)
λu2:T.λ:T.subst0 i u x0 u2
λ:T.λt2:T.subst0 (s (Flat Cast) 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 (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
case or3_intro0 : H11:ex2 T λu2:T.eq T t (THead (Flat Cast) 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 (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
we proceed by induction on H11 to prove or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
case ex_intro2 : x2:T H12:eq T t (THead (Flat Cast) x2 x1) H13:subst0 i u x0 x2 ⇒
the thesis becomes or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
(h1)
by (pr2_delta . . . . H1 . . H8 . H13)
pr2 c0 u1 x2
end of h1
(h2) by (pr2_free . . . H9) we proved pr2 c0 t1 x1
by (ex3_2_intro . . . . . . . H12 h1 h2)
we proved ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3
by (or_introl . . previous)
or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
case or3_intro1 : H11:ex2 T λt3:T.eq T t (THead (Flat Cast) x0 t3) λt3:T.subst0 (s (Flat Cast) i) u x1 t3 ⇒
the thesis becomes or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
we proceed by induction on H11 to prove or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
case ex_intro2 : x2:T H12:eq T t (THead (Flat Cast) x0 x2) H13:subst0 (s (Flat Cast) i) u x1 x2 ⇒
the thesis becomes or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
(h1) by (pr2_free . . . H8) we proved pr2 c0 u1 x0
(h2)
consider H13
we proved subst0 (s (Flat Cast) i) u x1 x2
that is equivalent to subst0 i u x1 x2
by (pr2_delta . . . . H1 . . H9 . previous)
pr2 c0 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 (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3
by (or_introl . . previous)
or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
case or3_intro2 : H11:ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.subst0 i u x0 u2 λ:T.λt3:T.subst0 (s (Flat Cast) i) u x1 t3 ⇒
the thesis becomes or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
we proceed by induction on H11 to prove or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
case ex3_2_intro : x2:T x3:T H12:eq T t (THead (Flat Cast) x2 x3) H13:subst0 i u x0 x2 H14:subst0 (s (Flat Cast) i) u x1 x3 ⇒
the thesis becomes or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
(h1)
by (pr2_delta . . . . H1 . . H8 . H13)
pr2 c0 u1 x2
end of h1
(h2)
consider H14
we proved subst0 (s (Flat Cast) i) u x1 x3
that is equivalent to subst0 i u x1 x3
by (pr2_delta . . . . H1 . . H9 . previous)
pr2 c0 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 (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3
by (or_introl . . previous)
or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
case or_intror : H6:pr0 t1 t2 ⇒
the thesis becomes or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
by (pr2_delta . . . . H1 . . H6 . H3)
we proved pr2 c0 t1 t
by (or_intror . . previous)
or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
we proved or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
∀H4:eq T t0 (THead (Flat Cast) u1 t1)
.or (ex3_2 T T λu2:T.λt3:T.eq T t (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c0 u1 u2 λ:T.λt3:T.pr2 c0 t1 t3) (pr2 c0 t1 t)
we proved
eq T y (THead (Flat Cast) u1 t1)
→or (ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Cast) u2 t2) λu2:T.λ:T.pr2 c u1 u2 λ:T.λt2:T.pr2 c t1 t2) (pr2 c t1 x)
we proved
∀y:T
.pr2 c y x
→(eq T y (THead (Flat Cast) u1 t1)
→or (ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Cast) u2 t2) λu2:T.λ:T.pr2 c u1 u2 λ:T.λt2:T.pr2 c t1 t2) (pr2 c t1 x))
by (insert_eq . . . . previous H)
we proved
or (ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Cast) u2 t2) λu2:T.λ:T.pr2 c u1 u2 λ:T.λt2:T.pr2 c t1 t2) (pr2 c t1 x)
we proved
∀c:C
.∀u1:T
.∀t1:T
.∀x:T
.pr2 c (THead (Flat Cast) u1 t1) x
→or (ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Cast) u2 t2) λu2:T.λ:T.pr2 c u1 u2 λ:T.λt2:T.pr2 c t1 t2) (pr2 c t1 x)