---

Step * 1 2 4 of Lemma int_add_grp_wf2


1. z : ℤ
⊢ monot(ℤ;x,y.x ≤ y;λw.(z + w))
BY
{ Eval ``monot`` 0 THEN Auto' }

---

Latex:

---

Latex:

1.  z  :  \mBbbZ{}
\mvdash{}  monot(\mBbbZ{};x,y.x  \mleq{}  y;\mlambda{}w.(z  +  w))


By

---

Latex:
Eval  ``monot``  0  THEN  Auto'

---

Home Index