---

Step * of Lemma member-nat-missing_wf

∀[i:ℕ]. ∀[s:nat-missing-type()].  (member-nat-missing(i;s) ∈ 𝔹)
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[i:\mBbbN{}].  \mforall{}[s:nat-missing-type()].    (member-nat-missing(i;s)  \mmember{}  \mBbbB{})


By

ProveWfLemma

---

Home Index