even stricter invariant
little progress on [Congruence.add_eq]

- partially merge cons info