---

Step * of Lemma on-loc-class-single-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:Id ─→ EClass(T)].
  single-valued-classrel(es;on-loc-class(X);T) supposing ∀i:Id. single-valued-classrel(es;X i;T)
BY
{ (Unfold `single-valued-classrel` 0
   THEN (UnivCD THENA MaAuto)
   THEN MaUseClassRel (-2)
   THEN MaUseClassRel (-1)
   THEN InstHyp [⌈loc(e)⌉;⌈e⌉;⌈v1⌉;⌈v2⌉] (-6)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X:Id  {}\mrightarrow{}  EClass(T)].
    single-valued-classrel(es;on-loc-class(X);T)  supposing  \mforall{}i:Id.  single-valued-classrel(es;X  i;T)


By

---

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

---

Home Index