---

Step * of Lemma mrec-spec_wf

∀[L:MutualRectypeSpec]. ∀[lbl,p:Atom].  (mrec-spec(L;lbl;p) ∈ (Atom + Atom + Type) List)
BY
{ (Unfold `mrec_spec` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[L:MutualRectypeSpec].  \mforall{}[lbl,p:Atom].    (mrec-spec(L;lbl;p)  \mmember{}  (Atom  +  Atom  +  Type)  List)


By

---

Latex:
(Unfold  `mrec\_spec`  0  THEN  ProveWfLemma)

---

Home Index