proposition: Lemma encode_morphism_and_ops `{Monoid_Morphism A B f}: @HomoMorphism sig (λ _, A) (λ _, B) _ _ ( _) ( _) (λ _, f).
proof: Proof. intros. apply encode_morphism_only. assumption. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics MathClasses.categories.categories