Nuprl - Pf event_msg_eq

E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2)

By: Analyze 0 THEN Unfold `event_msg_eq` 0 THEN Reduce 0 THEN Inst Thm* M:MessageStruct. EquivRel(|M|)(_1 =(M) _2) [MS(E)]

Generated subgoal:

1 1. E: EventStruct
2. EquivRel(|MS(E)|)(_1 =(MS(E)) _2)
EquivRel(|E|)((msg(E)(_1)) =(MS(E)) (msg(E)(_2)))

About: