---

Step * of Lemma pi-choices_wf

∀[t:pi_term()]. (pi-choices(t) ∈ (pi_prefix() × pi_term()) List)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[t:pi\_term()].  (pi-choices(t)  \mmember{}  (pi\_prefix()  \mtimes{}  pi\_term())  List)


By

---

Latex:
ProveWfLemma

---

Home Index