proposition: Lemma decode_morphism_and_ops `{InVariety theory x} `{InVariety theory y} `{!HomoMorphism theory x y f}: Monoid_Morphism (f tt).
proof: Proof. constructor; try apply _. constructor; try apply _. apply (preserves theory x y f mult). apply (preserves theory x y f one). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics MathClasses.categories.categories