---

Step * 1 2 1 of Lemma mobj-cases

.....assertion..... 
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)> ∈ mobj(S)
BY
{ SubsumeC ⌜i:Atom × mrec(S;i)⌝⋅ }

1
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)

2
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))
6. <k, mk-prec(lbl;t)> = <k, mk-prec(lbl;t)> ∈ (i:Atom × mrec(S;i))
⊢ (i:Atom × mrec(S;i)) ⊆r mobj(S)

---

Latex:

---

Latex:
.....assertion..... 
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{}  mobj(S)


By

---

Latex:
SubsumeC  \mkleeneopen{}i:Atom  \mtimes{}  mrec(S;i)\mkleeneclose{}\mcdot{}

---

Home Index