---

Step * of Lemma skip-first-class-is-empty-if-first

∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[X:EClass(A)].  Skip(X) es e ~ {} supposing ↑first(e)
BY
{ (Auto THEN RepUR ``skip-first-class`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[X:EClass(A)].    Skip(X)  es  e  \msim{}  \{\}  supposing  \muparrow{}first(e)


By

---

Latex:
(Auto  THEN  RepUR  ``skip-first-class``  0  THEN  AutoSplit)

---

Home Index