---

Step * of Lemma pe-loc_wf

∀[p:EO ⟶ ℙ']. ∀[e:PossibleEvent(p)].  (pe-loc(e) ∈ Id)
BY
{ (Unfold `pe-loc` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:EO  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[e:PossibleEvent(p)].    (pe-loc(e)  \mmember{}  Id)


By

---

Latex:
(Unfold  `pe-loc`  0  THEN  Auto)

---

Home Index