---

Step * 1 1 1 1 of Lemma mobj-ext


1. L : MutualRectypeSpec
2. i : Atom
3. x1 : mrec(L;i)
⊢ i ∈ {a:Atom| (a ∈ eager-map(λp.(fst(p));L))} 
BY
{ (pRecElim (-1) THEN (InstLemma `mrec-label-cases2` [⌜L⌝;⌜i⌝;⌜labl⌝]⋅ THENA Auto) THEN MemTypeCD THEN Try (Trivial)) }

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

---

Latex:

---

Latex:

1.  L  :  MutualRectypeSpec
2.  i  :  Atom
3.  x1  :  mrec(L;i)
\mvdash{}  i  \mmember{}  \{a:Atom|  (a  \mmember{}  eager-map(\mlambda{}p.(fst(p));L))\} 


By

---

Latex:
(pRecElim  (-1)
  THEN  (InstLemma  `mrec-label-cases2`  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}labl\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MemTypeCD
  THEN  Try  (Trivial))

---

Home Index