DEFINITION pr2_gen_ctail()
TYPE =
∀k:K
.∀c:C
.∀u:T
.∀t1:T
.∀t2:T
.pr2 (CTail k u c) t1 t2
→or (pr2 c t1 t2) (ex3 T λ:T.eq K k (Bind Abbr) λt:T.pr0 t1 t λt:T.subst0 (clen c) u t t2)
BODY =
assume k: K
assume c: C
assume u: T
assume t1: T
assume t2: T
suppose H: pr2 (CTail k u c) t1 t2
assume y: C
suppose H0: pr2 y t1 t2
we proceed by induction on H0 to prove
eq C y (CTail k u c)
→or (pr2 c t1 t2) (ex3 T λ:T.eq K k (Bind Abbr) λt3:T.pr0 t1 t3 λt3:T.subst0 (clen c) u t3 t2)
case pr2_free : c0:C t3:T t4:T H1:pr0 t3 t4 ⇒
the thesis becomes
eq C c0 (CTail k u c)
→or (pr2 c t3 t4) (ex3 T λ:T.eq K k (Bind Abbr) λt:T.pr0 t3 t λt:T.subst0 (clen c) u t t4)
suppose : eq C c0 (CTail k u c)
by (pr2_free . . . H1)
we proved pr2 c t3 t4
by (or_introl . . previous)
we proved or (pr2 c t3 t4) (ex3 T λ:T.eq K k (Bind Abbr) λt:T.pr0 t3 t λt:T.subst0 (clen c) u t t4)
eq C c0 (CTail k u c)
→or (pr2 c t3 t4) (ex3 T λ:T.eq K k (Bind Abbr) λt:T.pr0 t3 t λt:T.subst0 (clen c) u t t4)
case pr2_delta : c0:C d:C u0:T i:nat H1:getl i c0 (CHead d (Bind Abbr) u0) t3:T t4:T H2:pr0 t3 t4 t:T H3:subst0 i u0 t4 t ⇒
the thesis becomes
∀H4:eq C c0 (CTail k u c)
.or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
suppose H4: eq C c0 (CTail k u c)
(H5)
we proceed by induction on H4 to prove getl i (CTail k u c) (CHead d (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
getl i (CTail k u c) (CHead d (Bind Abbr) u0)
end of H5
(H_x)
by (getl_gen_tail . . . . . . . H5)
or
ex2 C λe:C.eq C d (CTail k u e) λe:C.getl i c (CHead e (Bind Abbr) u0)
ex4
nat
λ:nat.eq nat i (clen c)
λ:nat.eq K k (Bind Abbr)
λ:nat.eq T u u0
λn:nat.eq C d (CSort n)
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
case or_introl : H7:ex2 C λe:C.eq C d (CTail k u e) λe:C.getl i c (CHead e (Bind Abbr) u0) ⇒
the thesis becomes or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
we proceed by induction on H7 to prove or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
case ex_intro2 : x:C :eq C d (CTail k u x) H9:getl i c (CHead x (Bind Abbr) u0) ⇒
the thesis becomes or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
by (pr2_delta . . . . H9 . . H2 . H3)
we proved pr2 c t3 t
by (or_introl . . previous)
or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
case or_intror : H7:ex4 nat λ:nat.eq nat i (clen c) λ:nat.eq K k (Bind Abbr) λ:nat.eq T u u0 λn:nat.eq C d (CSort n) ⇒
the thesis becomes or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
we proceed by induction on H7 to prove or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
case ex4_intro : x0:nat H8:eq nat i (clen c) H9:eq K k (Bind Abbr) H10:eq T u u0 :eq C d (CSort x0) ⇒
the thesis becomes or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
(H12)
we proceed by induction on H8 to prove subst0 (clen c) u0 t4 t
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 (clen c) u0 t4 t
end of H12
(H13)
by (eq_ind_r . . . H12 . H10)
subst0 (clen c) u t4 t
end of H13
by (refl_equal . .)
we proved eq K (Bind Abbr) (Bind Abbr)
by (ex3_intro . . . . . previous H2 H13)
we proved ex3 T λ:T.eq K (Bind Abbr) (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t
by (or_intror . . previous)
we proved
or
pr2 c t3 t
ex3 T λ:T.eq K (Bind Abbr) (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t
by (eq_ind_r . . . previous . H9)
or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
we proved or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
∀H4:eq C c0 (CTail k u c)
.or (pr2 c t3 t) (ex3 T λ:T.eq K k (Bind Abbr) λt0:T.pr0 t3 t0 λt0:T.subst0 (clen c) u t0 t)
we proved
eq C y (CTail k u c)
→or (pr2 c t1 t2) (ex3 T λ:T.eq K k (Bind Abbr) λt3:T.pr0 t1 t3 λt3:T.subst0 (clen c) u t3 t2)
we proved
∀y:C
.pr2 y t1 t2
→(eq C y (CTail k u c)
→or (pr2 c t1 t2) (ex3 T λ:T.eq K k (Bind Abbr) λt3:T.pr0 t1 t3 λt3:T.subst0 (clen c) u t3 t2))
by (insert_eq . . . . previous H)
we proved or (pr2 c t1 t2) (ex3 T λ:T.eq K k (Bind Abbr) λt:T.pr0 t1 t λt:T.subst0 (clen c) u t t2)
we proved
∀k:K
.∀c:C
.∀u:T
.∀t1:T
.∀t2:T
.pr2 (CTail k u c) t1 t2
→or (pr2 c t1 t2) (ex3 T λ:T.eq K k (Bind Abbr) λt:T.pr0 t1 t λt:T.subst0 (clen c) u t t2)