add iff lemma for '✓ (to_agree a ⋅ to_agree b)'

This seems like such a clear characterization of agreement that I wonder why we do not have this already.