---

Step * of Lemma on-loc-class-es-sv

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:Id ─→ EClass(T)].
  es-sv-class(es;on-loc-class(X)) supposing ∀i:Id. es-sv-class(es;X i)
BY
{ (RepUR ``es-sv-class on-loc-class`` 0 THEN (UnivCD THENA MaAuto) THEN InstHyp [⌈loc(e)⌉;⌈e⌉] (-2)⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(RepUR  ``es-sv-class  on-loc-class``  0
  THEN  (UnivCD  THENA  MaAuto)
  THEN  InstHyp  [\mkleeneopen{}loc(e)\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  (-2)\mcdot{}
  THEN  Auto)

---

Home Index