---

Step * of Lemma hdf-ap-only-headers

∀[f:Name ─→ Type]. ∀[hdrs:Name List].
  ∀X:{X:msg-interface-hdf(f)| hdf-only-headers(f;hdrs;X)} . ∀m:Message(f).
    (fst(X(m)) ∈ {X:msg-interface-hdf(f)| hdf-only-headers(f;hdrs;X)} )
BY
{ (Unfold `msg-interface-hdf` 0 THEN Unfold `hdf-only-headers` 0 THEN Intros THEN BLemma `hdf-ap-invariant` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[hdrs:Name  List].
    \mforall{}X:\{X:msg-interface-hdf(f)|  hdf-only-headers(f;hdrs;X)\}  .  \mforall{}m:Message(f).
        (fst(X(m))  \mmember{}  \{X:msg-interface-hdf(f)|  hdf-only-headers(f;hdrs;X)\}  )


By

---

Latex:
(Unfold  `msg-interface-hdf`  0
  THEN  Unfold  `hdf-only-headers`  0
  THEN  Intros
  THEN  BLemma  `hdf-ap-invariant`
  THEN  Auto)

---

Home Index