E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2)M:MessageStruct. EquivRel(|M|)(_1 =(M) _2)f:(B
A), E:(AAProp).
EquivRel(A)(_1 E _2) 
EquivRel(B)((f(_1)) E (f(_2)))| Rank | Theorem | Name |
| 2 |
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) | [event_msg_eq_equiv] |
| cites | ||
| 1 |
Thm* M:MessageStruct. EquivRel(|M|)(_1 =(M) _2) | [msg_eq_equiv] |
| 0 |
Thm* f:(BA), E:(AAProp).
EquivRel(A)(_1 E _2) EquivRel(B)((f(_1)) E (f(_2))) | [induced_equiv_rel] |