---

Step * of Lemma classfun-res-base-classrel

∀[f:Name ─→ Type]. ∀[T:Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:T].
  (Base(hdr)@e = v ∈ T) supposing (v ∈ Base(hdr)(e) and hdr encodes T)
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "classfun-res-member-base" 0 THENA Auto)
   THEN Try ((Using [`T',⌈T⌉] (BLemma `assert-member-eclass`)⋅ THEN Auto THEN D 0 THEN InstConcl [⌈v⌉]⋅ THEN Auto))
   THEN MaUseClassRel (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[T:Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[hdr:Name].  \mforall{}[v:T].
    (Base(hdr)@e  =  v)  supposing  (v  \mmember{}  Base(hdr)(e)  and  hdr  encodes  T)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "classfun-res-member-base"  0  THENA  Auto)
  THEN  Try  ((Using  [`T',\mkleeneopen{}T\mkleeneclose{}]  (BLemma  `assert-member-eclass`)\mcdot{}
                        THEN  Auto
                        THEN  D  0
                        THEN  InstConcl  [\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
                        THEN  Auto))
  THEN  MaUseClassRel  (-1)
  THEN  Auto)

---

Home Index