---

Step * 1 of Lemma mobj-cases


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])
BY
{ D 0 }

1
1. [S] : MutualRectypeSpec
2. [P] : mobj(S) ⟶ TYPE
3. ∀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]

2
.....wf..... 
1. S : MutualRectypeSpec
2. P : mobj(S) ⟶ TYPE
⊢ istype(∀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)>])

---

Latex:

---

Latex:

1.  [S]  :  MutualRectypeSpec
2.  [P]  :  mobj(S)  {}\mrightarrow{}  TYPE
\mvdash{}  (\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:
D  0

---

Home Index