---

Step * of Lemma not-inl-sqeq-inr

∀[a,b:Base].  (¬(inl a ~ inr b ))
BY
{ (Auto THEN (Repeat (RW (SweepUpC CanonicalDiffC) 0) THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[a,b:Base].    (\mneg{}(inl  a  \msim{}  inr  b  ))


By

---

Latex:
(Auto  THEN  (Repeat  (RW  (SweepUpC  CanonicalDiffC)  0)  THEN  Auto)\mcdot{})

---

Home Index