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