---

Step * of Lemma message-cmp_wf

∀[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
  (message-cmp(hdrs;mcmp) ∈ comparison({m:Message(f)| (msg-header(m) ∈ hdrs)} ))
BY
{ (ProveWfLemma THEN RenameVar `xx' (-1) THEN InstLemma `msg-body-cmp_wf` [⌜f⌝;⌜hdrs⌝;⌜mcmp⌝;⌜xx⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[hdrs:Name  List].  \mforall{}[mcmp:hdr:Name  {}\mrightarrow{}  comparison(f  hdr)].
    (message-cmp(hdrs;mcmp)  \mmember{}  comparison(\{m:Message(f)|  (msg-header(m)  \mmember{}  hdrs)\}  ))


By

---

Latex:
(ProveWfLemma
  THEN  RenameVar  `xx'  (-1)
  THEN  InstLemma  `msg-body-cmp\_wf`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}hdrs\mkleeneclose{};\mkleeneopen{}mcmp\mkleeneclose{};\mkleeneopen{}xx\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index