Logically atomic triples: Notation, tactics, small example

This implements a proper infrastructure for logically atomic triples.

TODO:

• Get !161 (merged) merged.
• Get !167 (merged) merged and fix conflicts.
• CHANGELOG