---

Step * of Lemma tagged-list-messages_wf

∀[S,V:Type]. ∀[M:Id ⟶ Type]. ∀[s:S]. ∀[v:V]. ∀[L:(t:Id × (S ⟶ V ⟶ (M[t] List))) List].
  (tagged-list-messages(s;v;L) ∈ (t:Id × M[t]) List)
BY
{ (Unfold `tagged-list-messages` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[S,V:Type].  \mforall{}[M:Id  {}\mrightarrow{}  Type].  \mforall{}[s:S].  \mforall{}[v:V].  \mforall{}[L:(t:Id  \mtimes{}  (S  {}\mrightarrow{}  V  {}\mrightarrow{}  (M[t]  List)))  List].
    (tagged-list-messages(s;v;L)  \mmember{}  (t:Id  \mtimes{}  M[t])  List)


By

---

Latex:
(Unfold  `tagged-list-messages`  0  THEN  Auto)

---

Home Index