---

Step * of Lemma delivered-with-headers-no_repeats

∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdrs:Name List].
  no_repeats(E;filter(λe.header(e) ∈b hdrs);≤loc(e)))
BY
{ ((UnivCD THENA Auto) THEN (BLemma `no_repeats_filter` THENA Auto) THEN BLemma `es-le-before-no_repeats` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[hdrs:Name  List].
    no\_repeats(E;filter(\mlambda{}e.header(e)  \mmember{}\msubb{}  hdrs);\mleq{}loc(e)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (BLemma  `no\_repeats\_filter`  THENA  Auto)
  THEN  BLemma  `es-le-before-no\_repeats`
  THEN  Auto)

---

Home Index