---

Step * 2 of Lemma two-mul


1. ∀[x:ℤ]. (x + x ~ 2 * x)
⊢ ∀[x:Top]. (x + x ~ 2 * x)
BY
{ (SqReasoning
   THEN Try ((RWO "1" 0 THEN Complete (Auto)))
   THEN Try ((ExceptionSqequal (-1)
              THEN HypSubst' (-1) 0
              THEN RW (SubC (TagC (mk_tag_term 1))) 0
              THEN Complete (Auto)))) }

---

Latex:

---

Latex:

1.  \mforall{}[x:\mBbbZ{}].  (x  +  x  \msim{}  2  *  x)
\mvdash{}  \mforall{}[x:Top].  (x  +  x  \msim{}  2  *  x)


By

---

Latex:
(SqReasoning
  THEN  Try  ((RWO  "1"  0  THEN  Complete  (Auto)))
  THEN  Try  ((ExceptionSqequal  (-1)
                        THEN  HypSubst'  (-1)  0
                        THEN  RW  (SubC  (TagC  (mk\_tag\_term  1)))  0
                        THEN  Complete  (Auto))))

---

Home Index