---

{ [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:{tg:Id| M[tg]}   M[t]) List) }

{ Proof }

---

Definitions occuring in Statement :  tagged-list-messages: tagged-list-messages(s;v;L),  Id: Id,  uall: [x:A]. B[x],  so_apply: x[s],  member: t  T,  set: {x:A| B[x]} ,  function: x:A  B[x],  product: x:A  B[x],  list: type List,  universe: Type
Definitions :  uall: [x:A]. B[x],  so_apply: x[s],  member: t  T,  so_lambda: x.t[x],  uimplies: b supposing a
Lemmas :  tagged-list-messages_wf,  subtype_rel_list,  Id_wf

---

\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:\{tg:Id|  M[tg]\}    \mtimes{}  M[t])  List)


Date html generated: 2011_08_10-AM-07_47_15
Last ObjectModification: 2011_06_18-AM-08_12_41

Home Index