Step
*
of Lemma
lname_wf
∀[l:IdLnk]. (lname(l) ∈ Id)
BY
{ (Unfolds ``IdLnk lname`` 0 THEN Auto) }
Latex:
\mforall{}[l:IdLnk].  (lname(l)  \mmember{}  Id)
By
(Unfolds  ``IdLnk  lname``  0  THEN  Auto)
Home
Index