---

Step * of Lemma single-valued-classrel-implies-bag

∀[Info,T:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(T)]. ∀[e:E].
  (single-valued-classrel(es;X;T) ⇒ single-valued-bag(X es e;T))
BY
{ (Auto
   THEN Unfold `single-valued-classrel` (-1)
   THEN Unfold `single-valued-bag` 0
   THEN Auto
   THEN Try (Fold `classrel` (-1))
   THEN Try (Fold `classrel` (-2)⋅)
   THEN InstHyp [⌈e⌉;⌈x⌉;⌈y⌉] (-5)⋅
   THEN Auto) }

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(T)].  \mforall{}[e:E].
    (single-valued-classrel(es;X;T)  {}\mRightarrow{}  single-valued-bag(X  es  e;T))


By

(Auto
  THEN  Unfold  `single-valued-classrel`  (-1)
  THEN  Unfold  `single-valued-bag`  0
  THEN  Auto
  THEN  Try  (Fold  `classrel`  (-1))
  THEN  Try  (Fold  `classrel`  (-2)\mcdot{})
  THEN  InstHyp  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  (-5)\mcdot{}
  THEN  Auto)

---

Home Index