Thm* E:EventStruct, P:((Label (|E| List)) Prop).
( f,g:(Label (|E| List)). ( p:Label. g(p) f(p))  P(f)  P(g)) 
( f,g:(Label (|E| List)).
( a:|E|. p:Label. g(p) = filter( b. (b =msg=(E) a);f(p)))  P(f)  P(g))

( f,g,h:(Label (|E| List)).
( p,q:Label. ( x f(p).( y g(q). (x =msg=(E) y)))) 
( p:Label. h(p) = ((f(p)) @ (g(p))))  P(f)  P(g)  P(h))

switchable0(E)(local_deliver_property(E;P)) | [local_deliver_switchable] |