---

Step * of Lemma mobj-cases

∀[S:MutualRectypeSpec]. ∀[P:mobj(S) ⟶ TYPE].
  ((∀k:mKinds. ∀lbl:{lbl:Atom| 0 < ||mrec-spec(S;lbl;k)||} .
    ∀t:tuple-type(prec-arg-types(lbl,p.mrec-spec(S;lbl;p);k;lbl)).
      P[<k, mk-prec(lbl;t)>])
  ⇒ (∀x:mobj(S). P[x]))
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

1
1. [S] : MutualRectypeSpec
2. [P] : mobj(S) ⟶ TYPE
⊢ (∀k:mKinds. ∀lbl:{lbl:Atom| 0 < ||mrec-spec(S;lbl;k)||} .
   ∀t:tuple-type(prec-arg-types(lbl,p.mrec-spec(S;lbl;p);k;lbl)).
     P[<k, mk-prec(lbl;t)>])
⇒ (∀x:mobj(S). P[x])

---

Latex:

---

Latex:
\mforall{}[S:MutualRectypeSpec].  \mforall{}[P:mobj(S)  {}\mrightarrow{}  TYPE].
    ((\mforall{}k:mKinds.  \mforall{}lbl:\{lbl:Atom|  0  <  ||mrec-spec(S;lbl;k)||\}  .
        \mforall{}t:tuple-type(prec-arg-types(lbl,p.mrec-spec(S;lbl;p);k;lbl)).
            P[<k,  mk-prec(lbl;t)>])
    {}\mRightarrow{}  (\mforall{}x:mobj(S).  P[x]))


By

---

Latex:
RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index