Step
*
of Lemma
bound_in_prefix_wf
∀[pre:pi_prefix()]. (bound_in_prefix(pre) ∈ Name List)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[pre:pi\_prefix()].  (bound\_in\_prefix(pre)  \mmember{}  Name  List)
By
Latex:
ProveWfLemma
Home
Index