---

Step * of Lemma single-valued-base-classrel

∀[f:Name ─→ Type]. ∀[T:Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v1,v2:T]. ∀[hdr:Name].
  v1 ∈ Base(hdr)(e) ⇒ v2 ∈ Base(hdr)(e) ⇒ (v1 = v2 ∈ T) supposing T = (f hdr) ∈ Type
BY
{ ((UnivCD THENA Auto) THEN MaUseClassRel (-2) THEN MaUseClassRel (-1)) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[T:Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[v1,v2:T].  \mforall{}[hdr:Name].
    v1  \mmember{}  Base(hdr)(e)  {}\mRightarrow{}  v2  \mmember{}  Base(hdr)(e)  {}\mRightarrow{}  (v1  =  v2)  supposing  T  =  (f  hdr)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  MaUseClassRel  (-2)  THEN  MaUseClassRel  (-1))

---

Home Index