Step
*
of Lemma
es-locally-ordered_wf
∀[es:EO]. ∀[L:E List].  (es-locally-ordered(es;L) ∈ ℙ)
BY
{ ProveWfLemma }
Latex:
\mforall{}[es:EO].  \mforall{}[L:E  List].    (es-locally-ordered(es;L)  \mmember{}  \mBbbP{})
By
ProveWfLemma
Home
Index