---

Step * 1 1 1 of Lemma mobj-ext

.....assertion..... 
1. L : MutualRectypeSpec
2. i : Atom
3. x1 : mrec(L;i)
⊢ i ∈ mKinds
BY
{ Unfold `mkinds` 0 }

1
1. L : MutualRectypeSpec
2. i : Atom
3. x1 : mrec(L;i)
⊢ i ∈ {a:Atom| (a ∈ eager-map(λp.(fst(p));L))} 

---

Latex:

---

Latex:
.....assertion..... 
1.  L  :  MutualRectypeSpec
2.  i  :  Atom
3.  x1  :  mrec(L;i)
\mvdash{}  i  \mmember{}  mKinds


By

---

Latex:
Unfold  `mkinds`  0

---

Home Index