At: msg eq equiv 2
1. M: MessageStruct
2. EquivRel(|cEQ(M)|)(_1 =(cEQ(M)) _2)
3. a: |M|
4. b: |M|
5. (content(M)(a)) =(cEQ(M)) (content(M)(b))
6. sender(M)(a) =
sender(M)(b)
7. uid(M)(a) = uid(M)(b)
sender(M)(b) = sender(M)(a)
By:
EqLblFwd
THEN
HypSubst' -1 0
THEN
EqLblReflexive 0
Generated subgoals:None
About:
