---

Step * of Lemma not_all_sqequal

(∀[a,b:Base].  (a ~ b)) ⇒ False
BY
{ (Auto THEN (InstHyp [⌜0⌝;⌜1⌝] (-1)⋅ THENA Auto) THEN FLemma `not_zero_sqequal_one` [-1] THEN Auto)⋅ }

---

Latex:

---

Latex:
(\mforall{}[a,b:Base].    (a  \msim{}  b))  {}\mRightarrow{}  False


By

---

Latex:
(Auto  THEN  (InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  FLemma  `not\_zero\_sqequal\_one`  [-1]  THEN  Auto)\mcdot{}

---

Home Index