---

Step * of Lemma nullvar_wf

No Annotations
nullvar() ∈ varname()
BY
{ (SubsumeC ⌜Atom⌝⋅ THEN Auto THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
nullvar()  \mmember{}  varname()


By

---

Latex:
(SubsumeC  \mkleeneopen{}Atom\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  ProveWfLemma)

---

Home Index