First trivial structures: contradiction, equivalence.
Semigroup stuff.
Avoid public imports.
More structures and proofs.