At: msg eq equiv 3
1. M: MessageStruct
2. EquivRel(|cEQ(M)|)(_1 =(cEQ(M)) _2)
3. a: |M|
4. b: |M|
5. c: |M|
6. (content(M)(a)) =(cEQ(M)) (content(M)(b))
7. sender(M)(a) =
sender(M)(b)
8. uid(M)(a) = uid(M)(b)
9. (content(M)(b)) =(cEQ(M)) (content(M)(c))
10. sender(M)(b) = sender(M)(c)
11. uid(M)(b) = uid(M)(c)
(content(M)(a)) =(cEQ(M)) (content(M)(c))
By: UseTrans (content(M)(b))
Generated subgoals:None
About:
