---

Step * of Lemma mk-prec_wf-mrec

∀[L:MutualRectypeSpec]. ∀[i,labl:Atom]. ∀[x:tuple-type(prec-arg-types(lbl,p.mrec-spec(L;lbl;p);i;labl))].
  mk-prec(labl;x) ∈ mrec(L;i) supposing 0 < ||mrec-spec(L;labl;i)||
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[L:MutualRectypeSpec].  \mforall{}[i,labl:Atom].
\mforall{}[x:tuple-type(prec-arg-types(lbl,p.mrec-spec(L;lbl;p);i;labl))].
    mk-prec(labl;x)  \mmember{}  mrec(L;i)  supposing  0  <  ||mrec-spec(L;labl;i)||


By

---

Latex:
Auto

---

Home Index