---

Step * of Lemma mrec-label-cases

∀s:MutualRectypeSpec. ∀n:Atom. ∀lbl:{lbl:Atom| 0 < ||mrec-spec(s;lbl;n)||} .
  ((↑isl(apply-alist(AtomDeq;s;n))) ∧ (lbl ∈ map(λp.(fst(p));outl(apply-alist(AtomDeq;s;n)))))
BY
{ (Auto THEN Unfold `mrec_spec` 1 THEN DVar `lbl' THEN (Unhide THENA Auto)) }

1
1. s : (Atom × ((Atom × ((Atom + Atom + Type) List)) List)) List
2. n : Atom
3. lbl : Atom
4. 0 < ||mrec-spec(s;lbl;n)||
⊢ ↑isl(apply-alist(AtomDeq;s;n))

2
1. s : (Atom × ((Atom × ((Atom + Atom + Type) List)) List)) List
2. n : Atom
3. lbl : Atom
4. 0 < ||mrec-spec(s;lbl;n)||
5. ↑isl(apply-alist(AtomDeq;s;n))
⊢ (lbl ∈ map(λp.(fst(p));outl(apply-alist(AtomDeq;s;n))))

---

Latex:

---

Latex:
\mforall{}s:MutualRectypeSpec.  \mforall{}n:Atom.  \mforall{}lbl:\{lbl:Atom|  0  <  ||mrec-spec(s;lbl;n)||\}  .
    ((\muparrow{}isl(apply-alist(AtomDeq;s;n)))  \mwedge{}  (lbl  \mmember{}  map(\mlambda{}p.(fst(p));outl(apply-alist(AtomDeq;s;n)))))


By

---

Latex:
(Auto  THEN  Unfold  `mrec\_spec`  1  THEN  DVar  `lbl'  THEN  (Unhide  THENA  Auto))

---

Home Index