---

Step * of Lemma w-bars_wf

∀[A:Type]. ∀[w:co-w(A)]. ∀[p:ℕ ⟶ A].  (w-bars(w;p) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[w:co-w(A)].  \mforall{}[p:\mBbbN{}  {}\mrightarrow{}  A].    (w-bars(w;p)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index