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

At: msg eq equiv 1
1. M: MessageStruct
2. EquivRel(|cEQ(M)|)(_1 =(cEQ(M)) _2)
3. a: |M|

sender(M)(a) = sender(M)(a)
By: EqLblReflexive 0
Generated subgoals:

None

About:
assertapply

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