---

Step * 3 of Lemma posint_mul_mon_wf


Comm(ℕ+;λx,y. (x * y))
BY
{ UnfoldTopAb 0 THEN Reduce 0 THEN Auto }

---

Latex:

---

Latex:

Comm(\mBbbN{}\msupplus{};\mlambda{}x,y.  (x  *  y))


By

---

Latex:
UnfoldTopAb  0  THEN  Reduce  0  THEN  Auto

---

Home Index