---

Step * 3 of Lemma base-noloc-classrel2


1. T : Type
2. f : Name ─→ Type
3. es : EO+(Message(f))
4. e : E
5. v : T
6. hdr : Name
7. hdr encodes T
8. header(e) = hdr ∈ Name
9. v = msgval(e) ∈ T
⊢ v ∈ Base(hdr)(e)
BY
{ (RepUR ``classrel base-headers-msg-val cond-msg-body`` 0
   THEN Folds ``es-header es-info-body`` 0
   THEN AutoSplit
   THEN BagMemberD  0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  Name  {}\mrightarrow{}  Type
3.  es  :  EO+(Message(f))
4.  e  :  E
5.  v  :  T
6.  hdr  :  Name
7.  hdr  encodes  T
8.  header(e)  =  hdr
9.  v  =  msgval(e)
\mvdash{}  v  \mmember{}  Base(hdr)(e)


By

---

Latex:
(RepUR  ``classrel  base-headers-msg-val  cond-msg-body``  0
  THEN  Folds  ``es-header  es-info-body``  0
  THEN  AutoSplit
  THEN  BagMemberD    0
  THEN  Auto)

---

Home Index