DEFINITION pc3_fsubst0()
TYPE =
∀c1:C
.∀t1:T
.∀t:T
.pc3 c1 t1 t
→∀i:nat
.∀u:T.∀c2:C.∀t2:T.(fsubst0 i u c1 t1 c2 t2)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t2 t)
BODY =
assume c1: C
assume t1: T
assume t: T
suppose H: pc3 c1 t1 t
(h1)
assume t0: T
assume i: nat
assume u: T
assume c2: C
assume t2: T
suppose H0: fsubst0 i u c1 t0 c2 t2
we proceed by induction on H0 to prove ∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t2 t0)
case fsubst0_snd : t3:T H1:subst0 i u t0 t3 ⇒
the thesis becomes ∀e:C.∀H2:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c1 t3 t0)
assume e: C
suppose H2: getl i c1 (CHead e (Bind Abbr) u)
by (pr0_refl .)
we proved pr0 t0 t0
by (pr2_delta . . . . H2 . . previous . H1)
we proved pr2 c1 t0 t3
by (pc3_pr2_x . . . previous)
we proved pc3 c1 t3 t0
∀e:C.∀H2:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c1 t3 t0)
case fsubst0_fst : c0:C :csubst0 i u c1 c0 ⇒
the thesis becomes ∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c0 t0 t0)
assume e: C
suppose : getl i c1 (CHead e (Bind Abbr) u)
by (pc3_refl . .)
we proved pc3 c0 t0 t0
∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c0 t0 t0)
case fsubst0_both : t3:T H1:subst0 i u t0 t3 c0:C H2:csubst0 i u c1 c0 ⇒
the thesis becomes ∀e:C.∀H3:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c0 t3 t0)
assume e: C
suppose H3: getl i c1 (CHead e (Bind Abbr) u)
(h1)
by (le_n .)
we proved le i i
by (csubst0_getl_ge . . previous . . . H2 . H3)
getl i c0 (CHead e (Bind Abbr) u)
end of h1
(h2) by (pr0_refl .) we proved pr0 t0 t0
by (pr2_delta . . . . h1 . . h2 . H1)
we proved pr2 c0 t0 t3
by (pc3_pr2_x . . . previous)
we proved pc3 c0 t3 t0
∀e:C.∀H3:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c0 t3 t0)
we proved ∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t2 t0)
∀t0:T
.∀i:nat
.∀u:T.∀c2:C.∀t2:T.(fsubst0 i u c1 t0 c2 t2)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t2 t0)
end of h1
(h2)
assume t0: T
assume t2: T
suppose H0: pr2 c1 t0 t2
assume t3: T
suppose H1: pc3 c1 t2 t3
suppose H2:
∀i:nat
.∀u:T.∀c2:C.∀t4:T.(fsubst0 i u c1 t2 c2 t4)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t4 t3)
assume i: nat
assume u: T
assume c2: C
assume t4: T
suppose H3: fsubst0 i u c1 t0 c2 t4
we proceed by induction on H3 to prove ∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t4 t3)
case fsubst0_snd : t5:T H4:subst0 i u t0 t5 ⇒
the thesis becomes ∀e:C.∀H5:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c1 t5 t3)
assume e: C
suppose H5: getl i c1 (CHead e (Bind Abbr) u)
by (fsubst0_snd . . . . . H4)
we proved fsubst0 i u c1 t0 c1 t5
by (pc3_pr2_fsubst0 . . . H0 . . . . previous . H5)
we proved pc3 c1 t5 t2
by (pc3_t . . . previous . H1)
we proved pc3 c1 t5 t3
∀e:C.∀H5:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c1 t5 t3)
case fsubst0_fst : c0:C H4:csubst0 i u c1 c0 ⇒
the thesis becomes ∀e:C.∀H5:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c0 t0 t3)
assume e: C
suppose H5: getl i c1 (CHead e (Bind Abbr) u)
(h1)
by (fsubst0_fst . . . . . H4)
we proved fsubst0 i u c1 t0 c0 t0
by (pc3_pr2_fsubst0 . . . H0 . . . . previous . H5)
pc3 c0 t0 t2
end of h1
(h2)
by (fsubst0_fst . . . . . H4)
we proved fsubst0 i u c1 t2 c0 t2
by (H2 . . . . previous . H5)
pc3 c0 t2 t3
end of h2
by (pc3_t . . . h1 . h2)
we proved pc3 c0 t0 t3
∀e:C.∀H5:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c0 t0 t3)
case fsubst0_both : t5:T H4:subst0 i u t0 t5 c0:C H5:csubst0 i u c1 c0 ⇒
the thesis becomes ∀e:C.∀H6:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c0 t5 t3)
assume e: C
suppose H6: getl i c1 (CHead e (Bind Abbr) u)
(h1)
by (fsubst0_both . . . . . H4 . H5)
we proved fsubst0 i u c1 t0 c0 t5
by (pc3_pr2_fsubst0 . . . H0 . . . . previous . H6)
pc3 c0 t5 t2
end of h1
(h2)
by (fsubst0_fst . . . . . H5)
we proved fsubst0 i u c1 t2 c0 t2
by (H2 . . . . previous . H6)
pc3 c0 t2 t3
end of h2
by (pc3_t . . . h1 . h2)
we proved pc3 c0 t5 t3
∀e:C.∀H6:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c0 t5 t3)
we proved ∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t4 t3)
∀t0:T
.∀t2:T
.pr2 c1 t0 t2
→∀t3:T
.pc3 c1 t2 t3
→(∀i:nat
.∀u:T.∀c2:C.∀t4:T.(fsubst0 i u c1 t2 c2 t4)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t4 t3)
→∀i:nat
.∀u:T.∀c2:C.∀t4:T.(fsubst0 i u c1 t0 c2 t4)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t4 t3))
end of h2
(h3)
assume t0: T
assume t2: T
suppose H0: pr2 c1 t0 t2
assume t3: T
suppose H1: pc3 c1 t0 t3
suppose H2:
∀i:nat
.∀u:T.∀c2:C.∀t4:T.(fsubst0 i u c1 t0 c2 t4)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t4 t3)
assume i: nat
assume u: T
assume c2: C
assume t4: T
suppose H3: fsubst0 i u c1 t2 c2 t4
we proceed by induction on H3 to prove ∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t4 t3)
case fsubst0_snd : t5:T H4:subst0 i u t2 t5 ⇒
the thesis becomes ∀e:C.∀H5:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c1 t5 t3)
assume e: C
suppose H5: getl i c1 (CHead e (Bind Abbr) u)
by (fsubst0_snd . . . . . H4)
we proved fsubst0 i u c1 t2 c1 t5
by (pc3_pr2_fsubst0_back . . . H0 . . . . previous . H5)
we proved pc3 c1 t0 t5
by (pc3_s . . . previous)
we proved pc3 c1 t5 t0
by (pc3_t . . . previous . H1)
we proved pc3 c1 t5 t3
∀e:C.∀H5:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c1 t5 t3)
case fsubst0_fst : c0:C H4:csubst0 i u c1 c0 ⇒
the thesis becomes ∀e:C.∀H5:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c0 t2 t3)
assume e: C
suppose H5: getl i c1 (CHead e (Bind Abbr) u)
(h1)
by (fsubst0_fst . . . . . H4)
we proved fsubst0 i u c1 t2 c0 t2
by (pc3_pr2_fsubst0_back . . . H0 . . . . previous . H5)
we proved pc3 c0 t0 t2
by (pc3_s . . . previous)
pc3 c0 t2 t0
end of h1
(h2)
by (fsubst0_fst . . . . . H4)
we proved fsubst0 i u c1 t0 c0 t0
by (H2 . . . . previous . H5)
pc3 c0 t0 t3
end of h2
by (pc3_t . . . h1 . h2)
we proved pc3 c0 t2 t3
∀e:C.∀H5:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c0 t2 t3)
case fsubst0_both : t5:T H4:subst0 i u t2 t5 c0:C H5:csubst0 i u c1 c0 ⇒
the thesis becomes ∀e:C.∀H6:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c0 t5 t3)
assume e: C
suppose H6: getl i c1 (CHead e (Bind Abbr) u)
(h1)
by (fsubst0_both . . . . . H4 . H5)
we proved fsubst0 i u c1 t2 c0 t5
by (pc3_pr2_fsubst0_back . . . H0 . . . . previous . H6)
we proved pc3 c0 t0 t5
by (pc3_s . . . previous)
pc3 c0 t5 t0
end of h1
(h2)
by (fsubst0_fst . . . . . H5)
we proved fsubst0 i u c1 t0 c0 t0
by (H2 . . . . previous . H6)
pc3 c0 t0 t3
end of h2
by (pc3_t . . . h1 . h2)
we proved pc3 c0 t5 t3
∀e:C.∀H6:(getl i c1 (CHead e (Bind Abbr) u)).(pc3 c0 t5 t3)
we proved ∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t4 t3)
∀t0:T
.∀t2:T
.pr2 c1 t0 t2
→∀t3:T
.pc3 c1 t0 t3
→(∀i:nat
.∀u:T.∀c2:C.∀t4:T.(fsubst0 i u c1 t0 c2 t4)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t4 t3)
→∀i:nat
.∀u:T.∀c2:C.∀t4:T.(fsubst0 i u c1 t2 c2 t4)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t4 t3))
end of h3
by (pc3_ind_left . . h1 h2 h3 . . H)
we proved
∀i:nat
.∀u:T.∀c2:C.∀t3:T.(fsubst0 i u c1 t1 c2 t3)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t3 t)
we proved
∀c1:C
.∀t1:T
.∀t:T
.pc3 c1 t1 t
→∀i:nat
.∀u:T.∀c2:C.∀t3:T.(fsubst0 i u c1 t1 c2 t3)→∀e:C.(getl i c1 (CHead e (Bind Abbr) u))→(pc3 c2 t3 t)