---

Step * of Lemma singleton-nat-missing-prop

∀x,y:ℕ.  (↑member-nat-missing(x;singleton-nat-missing(y)) ⇐⇒ x = y ∈ ℕ)
BY
{ (Auto
   THEN (All(RWO "assert-member-nat-missing") THENA Auto)
   THEN All(RepUR ``singleton-nat-missing``)
   THEN Auto
   THEN All(RW ListC)
   THEN Auto
   THEN Try ((RWO "not_over_and" (-1) THENA Auto))
   THEN Try ((DNot 0 THENA Auto))
   THEN Try (DProdsAndUnions)
   THEN Auto) }

---

Latex:


\mforall{}x,y:\mBbbN{}.    (\muparrow{}member-nat-missing(x;singleton-nat-missing(y))  \mLeftarrow{}{}\mRightarrow{}  x  =  y)


By

(Auto
  THEN  (All(RWO  "assert-member-nat-missing")  THENA  Auto)
  THEN  All(RepUR  ``singleton-nat-missing``)
  THEN  Auto
  THEN  All(RW  ListC)
  THEN  Auto
  THEN  Try  ((RWO  "not\_over\_and"  (-1)  THENA  Auto))
  THEN  Try  ((DNot  0  THENA  Auto))
  THEN  Try  (DProdsAndUnions)
  THEN  Auto)

---

Home Index