---

Step * 1 2 of Lemma mobj-cases

.....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)>])
BY
{ (D 0
   THENL [Auto
         ; (D 0 THENL [Auto; (D 0 THENL [(D -2 THEN Auto); (Assert ⌜<k, mk-prec(lbl;t)> ∈ mobj(S)⌝⋅ THENM Auto)])])]
) }

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

---

Latex:

---

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


By

---

Latex:
(D  0
  THENL  [Auto
              ;  (D  0
                    THENL  [Auto
                                ;  (D  0
                                      THENL  [(D  -2  THEN  Auto);  (Assert  \mkleeneopen{}<k,  mk-prec(lbl;t)>  \mmember{}  mobj(S)\mkleeneclose{}\mcdot{}  THENM  Auto)]
                                )]
              )]
)

---

Home Index