proposition: Lemma encode_algebra_only `{!AlgebraOps theory A} `{∀ u, Equiv (A u)} `{!SemiGroup (A tt)}: Algebra theory A .
proof: Proof. constructor; intros []; simpl in *; try apply _. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics categories.categories