(2steps) PrintForm Definitions Lemmas mb structures Sections GenAutomata Doc

At: event msg eq equiv 1
1. E: EventStruct
2. EquivRel(|MS(E)|)(_1 =(MS(E)) _2)

EquivRel(|E|)((msg(E)(_1)) =(MS(E)) (msg(E)(_2)))
By:
Inst Thm* f:(BA), E:(AAProp). EquivRel(A)(_1 E _2) EquivRel(B)((f(_1)) E (f(_2))) [|MS(E)|;|E|;msg(E);x,y. x =(MS(E)) y]
THEN
All Reduce
Generated subgoals:

None

About:
assertlambdaapply

(2steps) PrintForm Definitions Lemmas mb structures Sections GenAutomata Doc