---

Step * of Lemma msgs-interface-delivered_wf

∀[f:Name ─→ Type]. ∀X:EClass(Interface). (msgs-interface-delivered{i:l}(X;f) ∈ ℙ')
BY
{ WithCumulativity(ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}X:EClass(Interface).  (msgs-interface-delivered\{i:l\}(X;f)  \mmember{}  \mBbbP{}')


By

---

Latex:
WithCumulativity(ProveWfLemma)

---

Home Index