Step
*
of Lemma
pi-names_wf
∀[p:pi_term()]. (pi-names(p) ∈ Name List)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[p:pi\_term()].  (pi-names(p)  \mmember{}  Name  List)
By
Latex:
ProveWfLemma
Home
Index