---

Step * of Lemma base-not-discrete

¬discrete-type(Base)
BY
{ ((D 0 THENA Auto)
   THEN (InstLemma `strong-subtype-discrete-type` [⌜partial(ℤ)⌝;⌜Base⌝]⋅ THENA EAuto 1)
   THEN MoveToConcl (-1)
   THEN Fold `not` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mneg{}discrete-type(Base)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma  `strong-subtype-discrete-type`  [\mkleeneopen{}partial(\mBbbZ{})\mkleeneclose{};\mkleeneopen{}Base\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
  THEN  MoveToConcl  (-1)
  THEN  Fold  `not`  0
  THEN  Auto)

---

Home Index