---

Step * of Lemma ocmon_6

∀[g:OCMon]. ∀[z:|g|].  monot(|g|;x,y.↑(x ≤b y);λw.(z * w))
BY
{ ((ProvePropertyLemma `none` 1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g:OCMon].  \mforall{}[z:|g|].    monot(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w))


By

---

Latex:
((ProvePropertyLemma  `none`  1)  THEN  Auto)

---

Home Index