---

Step * 1 1 of Lemma mobj-cases


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]
BY
{ ((D 0 THENA Auto) THEN (InstLemma  `mobj-sq` [⌜S⌝;⌜x⌝]⋅ THENA Auto) THEN HypSubst' (-1) 0 THEN BHyp 3 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma    `mobj-sq`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  BHyp  3
  THEN  Auto)

---

Home Index