---

Step * of Lemma empty-nat-missing-prop

∀x:ℕ. (¬↑member-nat-missing(x;empty-nat-missing()))
BY
{ (RepUR ``member-nat-missing empty-nat-missing`` 0 THEN Auto THEN AllPushDown THEN D 0 THEN Auto) }

---

Latex:


\mforall{}x:\mBbbN{}.  (\mneg{}\muparrow{}member-nat-missing(x;empty-nat-missing()))


By

(RepUR  ``member-nat-missing  empty-nat-missing``  0  THEN  Auto  THEN  AllPushDown  THEN  D  0  THEN  Auto)

---

Home Index