---

Step * of Lemma itermMinus_functionality

∀[a,b:int_term()].  "-"a ≡ "-"b supposing a ≡ b
BY
{ (Auto THEN RepeatFor 2 (ParallelLast) THEN (RepUR ``int_term_value`` 0 THEN Fold `int_term_value` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:int\_term()].    "-"a  \mequiv{}  "-"b  supposing  a  \mequiv{}  b


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (RepUR  ``int\_term\_value``  0  THEN  Fold  `int\_term\_value`  0)
  THEN  Auto)

---

Home Index