Step
*
of Lemma
first-class_wf
∀[Info,A:Type]. ∀[L:EClass(A) List].  (first-class(L) ∈ EClass(A))
BY
{ ProveWfLemma }
Latex:
\mforall{}[Info,A:Type].  \mforall{}[L:EClass(A)  List].    (first-class(L)  \mmember{}  EClass(A))
By
ProveWfLemma
Home
Index