---

Step * of Lemma inverse-inverse-letters

∀[X:Type]. ∀[a,b,c:X + X].  (a = -b ⇒ c = -a ⇒ (c = b ∈ (X + X)))
BY
{ (Auto THEN (All (RepUR  ``inverse-letters``) THEN ExRepD) THEN SplitOrHyps THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[a,b,c:X  +  X].    (a  =  -b  {}\mRightarrow{}  c  =  -a  {}\mRightarrow{}  (c  =  b))


By

---

Latex:
(Auto  THEN  (All  (RepUR    ``inverse-letters``)  THEN  ExRepD)  THEN  SplitOrHyps  THEN  Auto)

---

Home Index