Step * of Lemma ocmon_refl

[g:OCMon]. ∀[a:|g|].  (↑(a ≤b a))
BY
((ProvePropertyLemma `refl` 1) THEN Auto) }


Latex:


Latex:
\mforall{}[g:OCMon].  \mforall{}[a:|g|].    (\muparrow{}(a  \mleq{}\msubb{}  a))


By


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




Home Index