---

Step * 1 2 1 1 of Lemma mobj-cases


1. S : MutualRectypeSpec
2. P : mobj(S) ⟶ TYPE
3. k : mKinds
4. lbl : {lbl:Atom| 0 < ||mrec-spec(S;lbl;k)||} 
5. t : tuple-type(prec-arg-types(lbl,p.mrec-spec(S;lbl;p);k;lbl))
⊢ <k, mk-prec(lbl;t)> ∈ i:Atom × mrec(S;i)
BY
{ (D 3 THEN Auto) }

---

Latex:

---

Latex:

1.  S  :  MutualRectypeSpec
2.  P  :  mobj(S)  {}\mrightarrow{}  TYPE
3.  k  :  mKinds
4.  lbl  :  \{lbl:Atom|  0  <  ||mrec-spec(S;lbl;k)||\} 
5.  t  :  tuple-type(prec-arg-types(lbl,p.mrec-spec(S;lbl;p);k;lbl))
\mvdash{}  <k,  mk-prec(lbl;t)>  \mmember{}  i:Atom  \mtimes{}  mrec(S;i)


By

---

Latex:
(D  3  THEN  Auto)

---

Home Index