---

Step * of Lemma base-noloc-classrel

∀[T:Type]. ∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v:T]. ∀[hdr:Name].
  uiff(v ∈ Base(hdr)(e);(header(e) = hdr ∈ Name) ∧ has-es-info-type(es;e;f;T) ∧ (v = msgval(e) ∈ T)) 
  supposing hdr encodes T
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
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. v ∈ Base(hdr)(e)
⊢ (header(e) = hdr ∈ Name) ∧ has-es-info-type(es;e;f;T) ∧ (v = msgval(e) ∈ T)

2
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) ∧ has-es-info-type(es;e;f;T) ∧ (v = msgval(e) ∈ T)
⊢ v ∈ Base(hdr)(e)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[v:T].  \mforall{}[hdr:Name].
    uiff(v  \mmember{}  Base(hdr)(e);(header(e)  =  hdr)  \mwedge{}  has-es-info-type(es;e;f;T)  \mwedge{}  (v  =  msgval(e))) 
    supposing  hdr  encodes  T


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index