---

Step * of Lemma hdf-ap-single-valued-except

∀[f:Name ─→ Type]. ∀[hdrs:Name List]. ∀[X:{X:msg-interface-hdf(f)| hdf-single-valued-except(f;hdrs;X)} ].
  ∀m:Message(f). (fst(X(m)) ∈ {X:msg-interface-hdf(f)| hdf-single-valued-except(f;hdrs;X)} )
BY
{ (Intros
   THEN Unhide
   THEN Unfold `hdf-single-valued-except` 0
   THEN Unfold `msg-interface-hdf` 0
   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-single-valued-except(f;hdrs;X)\}  ].
    \mforall{}m:Message(f).  (fst(X(m))  \mmember{}  \{X:msg-interface-hdf(f)|  hdf-single-valued-except(f;hdrs;X)\}  )


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  Unfold  `hdf-single-valued-except`  0
  THEN  Unfold  `msg-interface-hdf`  0
  THEN  BLemma  `hdf-ap-invariant`
  THEN  Auto)

---

Home Index