---

Step * of Lemma num-var_wf

No Annotations
∀[t:Atom]. ∀[n:ℕ].  (t_n ∈ varname())
BY
{ (Unfold `varname` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[t:Atom].  \mforall{}[n:\mBbbN{}].    (t\_n  \mmember{}  varname())


By

---

Latex:
(Unfold  `varname`  0  THEN  ProveWfLemma)

---

Home Index