At: msg eq equiv 4
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)
sender(M)(a) = sender(M)(c)
By:
AssertBY (sender(M)(a) = sender(M)(c)) EqLblFwd
THEN
HypSubst' -1 0
THEN
EqLblReflexive 0
Generated subgoals:None
About:
