---

Step * of Lemma itermMinus_functionality_wrt_req

∀[a,b:int_term()].  "-"a ≡ "-"b supposing a ≡ b
BY
{ (Auto
   THEN RepeatFor 2 (ParallelLast)
   THEN (RepUR ``real_term_value`` 0 THEN Fold `real_term_value` 0)
   THEN Auto
   THEN RWO "-1" 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  ``real\_term\_value``  0  THEN  Fold  `real\_term\_value`  0)
  THEN  Auto
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index