Step
*
of Lemma
es-prior-interface_wf
∀[Info:Type]. ∀[X:EClass(Top)].  (prior(X) ∈ EClass(E(X)))
BY
{ Auto }
Latex:
Latex:
\mforall{}[Info:Type].  \mforall{}[X:EClass(Top)].    (prior(X)  \mmember{}  EClass(E(X)))
By
Latex:
Auto
Home
Index