---

Step * of Lemma eclass_wf3

∀[f:Name ─→ Type]. ∀[T:Type].  (EClass(T) ∈ 𝕌')
BY
{ (Auto THEN skip{(RepUR ``eclass event-ordering+`` 0 THEN Auto)}) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[T:Type].    (EClass(T)  \mmember{}  \mBbbU{}')


By

---

Latex:
(Auto  THEN  skip\{(RepUR  ``eclass  event-ordering+``  0  THEN  Auto)\})

---

Home Index