---

Step * of Lemma alle-at-not-first

∀es:EO. ∀i:Id.  ∀[P:{e:E| loc(e) = i ∈ Id}  ─→ ℙ]. (∀e@i.P[e] ⇒ ∀e@i.P[pred(e)] supposing ¬↑first(e))
BY
{ (Auto THEN (All (Unfold `alle-at`)) THEN Auto THEN BackThruSomeHyp THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}i:Id.    \mforall{}[P:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}].  (\mforall{}e@i.P[e]  {}\mRightarrow{}  \mforall{}e@i.P[pred(e)]  supposing  \mneg{}\muparrow{}first(e))


By

(Auto  THEN  (All  (Unfold  `alle-at`))  THEN  Auto  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index