---

Step * of Lemma primed-class-opt-single-val

∀[Info,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(B)]. ∀[init:Id ⟶ bag(B)].
  ((∀l:Id. single-valued-bag(init l;B)) ⇒ single-valued-classrel(es;X;B) ⇒ single-valued-classrel(es;Prior(X)?init;B))
BY
{ (InstLemma `primed-class-opt-single-val0` []
   THEN RepeatFor 5 (ParallelLast)
   THEN Auto
   THEN Unfold `single-valued-classrel` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(B)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].
    ((\mforall{}l:Id.  single-valued-bag(init  l;B))
    {}\mRightarrow{}  single-valued-classrel(es;X;B)
    {}\mRightarrow{}  single-valued-classrel(es;Prior(X)?init;B))


By

---

Latex:
(InstLemma  `primed-class-opt-single-val0`  []
  THEN  RepeatFor  5  (ParallelLast)
  THEN  Auto
  THEN  Unfold  `single-valued-classrel`  0
  THEN  Auto)

---

Home Index