---

Step * 1 1 1 1 1 of Lemma mobj-ext

.....wf..... 
1. L : MutualRectypeSpec
2. i : Atom
3. labl : {lbl:Atom| 0 < ||mrec-spec(L;lbl;i)||} 
4. x2 : tuple-type(map(λx.case x
                           of inl(y) =>
                           case y
                            of inl(p) =>
                            prec(lbl,p.mrec-spec(L;lbl;p);p)
                            | inr(p) =>
                            prec(lbl,p.mrec-spec(L;lbl;p);p) List
                           | inr(E) =>
                           E;mrec-spec(L;labl;i)))
5. (i ∈ eager-map(λp.(fst(p));L))
6. a : Atom
⊢ istype((a ∈ eager-map(λp.(fst(p));L)))
BY
{ (UnfoldTopAb 1 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  L  :  MutualRectypeSpec
2.  i  :  Atom
3.  labl  :  \{lbl:Atom|  0  <  ||mrec-spec(L;lbl;i)||\} 
4.  x2  :  tuple-type(map(\mlambda{}x.case  x
                                                      of  inl(y)  =>
                                                      case  y
                                                        of  inl(p)  =>
                                                        prec(lbl,p.mrec-spec(L;lbl;p);p)
                                                        |  inr(p)  =>
                                                        prec(lbl,p.mrec-spec(L;lbl;p);p)  List
                                                      |  inr(E)  =>
                                                      E;mrec-spec(L;labl;i)))
5.  (i  \mmember{}  eager-map(\mlambda{}p.(fst(p));L))
6.  a  :  Atom
\mvdash{}  istype((a  \mmember{}  eager-map(\mlambda{}p.(fst(p));L)))


By

---

Latex:
(UnfoldTopAb  1  THEN  Auto)

---

Home Index