a little work on [Congruence.add_eq]

- done with Rasmus
- it's like propagate, but we try to maintain a stronger invariant
- not finished