---

Step * 2 of Lemma posint_mul_mon_wf


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

---

Latex:

---

Latex:

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


By

---

Latex:
UnfoldTopAb  0  THEN  Reduce  0  THEN  Auto

---

Home Index