---

Step * of Lemma processChoose_wf2

∀[l_comm:Id]. (processChoose(l_comm) ∈ pi-process())
BY
{ ((Assert [] ∈ ℕ List BY Auto) THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[l$_{comm}$:Id].  (processChoose(l$_{comm}$)  \mmember{}  pi-process())


By

---

Latex:
((Assert  []  \mmember{}  \mBbbN{}  List  BY  Auto)  THEN  ProveWfLemma)

---

Home Index