---

Step * of Lemma abs-val_wf

∀[x:ℤ]. (|x| ∈ ℕ)
BY
{ Auto THEN Unfold `abs-val` 0 THEN SplitOnConclITE THEN Auto }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  (|x|  \mmember{}  \mBbbN{})


By

---

Latex:
Auto  THEN  Unfold  `abs-val`  0  THEN  SplitOnConclITE  THEN  Auto

---

Home Index