---

Step * of Lemma bdd-diff_weakening

∀a,b:ℕ+ ⟶ ℤ.  ((a = b ∈ (ℕ+ ⟶ ℤ)) ⇒ bdd-diff(a;b))
BY
{ (InstLemma `bdd-diff-equiv` [] THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.    ((a  =  b)  {}\mRightarrow{}  bdd-diff(a;b))


By

---

Latex:
(InstLemma  `bdd-diff-equiv`  []  THEN  Auto)\mcdot{}

---

Home Index