---

Step * of Lemma int-add-exception

∀[x:ℤ]. ∀[u,v:Top].  (x + (exception(u; v)) ~ exception(u; v))
BY
{ TACTIC:((UnivCD THENA Auto) THEN Refine_exceptionAdd THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  \mforall{}[u,v:Top].    (x  +  (exception(u;  v))  \msim{}  exception(u;  v))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  Refine\_exceptionAdd  THEN  Auto)

---

Home Index