---

Step * of Lemma class-at-single-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T)]. ∀[locs:bag(Id)].
  single-valued-classrel(es;X@locs;T) supposing single-valued-classrel(es;X;T)
BY
{ (Unfold `single-valued-classrel` 0
   THEN (UnivCD THENA MaAuto)
   THEN MaUseClassRel (-2)
   THEN MaUseClassRel (-1)
   THEN InstHyp [⌜e⌝;⌜v1⌝;⌜v2⌝] (-8)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[locs:bag(Id)].
    single-valued-classrel(es;X@locs;T)  supposing  single-valued-classrel(es;X;T)


By

---

Latex:
(Unfold  `single-valued-classrel`  0
  THEN  (UnivCD  THENA  MaAuto)
  THEN  MaUseClassRel  (-2)
  THEN  MaUseClassRel  (-1)
  THEN  InstHyp  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{}]  (-8)\mcdot{}
  THEN  Auto)

---

Home Index