(14steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: switchable induced 8
1. E: EventStruct
2. A: Type
3. f: A|E|
4. P: (|E| List)Prop
5. tr:|E| List. P(tr) No-dup-deliver(E)(tr)

tr:A List. P(map(f;tr)) No-dup-deliver(induced_event_str(E;A;f))(tr)
By:
All (h.(Unfolds [`induced_event_str`;`P_no_dup`] h) THEN (Reduce h))
THEN
All (h.(Unfold `event_msg_eq` h) THEN (Reduce h))
THEN
AllHyps (InstHyp [map(f;tr);i;j])
THEN
Try (RWO "map_select" 0)
THEN
Try (RWO "map_length" 0)
Generated subgoals:

None

About:
listapplyfunctionuniversepropimpliesall

(14steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc