---

Step * of Lemma union-nat-missing-pos_wf

∀[s1:nat-missing-type()]. ∀[max:ℕ]. ∀[missing:ℕ List].  (union-nat-missing-pos(s1;max;missing) ∈ nat-missing-type())
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[s1:nat-missing-type()].  \mforall{}[max:\mBbbN{}].  \mforall{}[missing:\mBbbN{}  List].
    (union-nat-missing-pos(s1;max;missing)  \mmember{}  nat-missing-type())


By

---

Latex:
ProveWfLemma

---

Home Index