proposition: Lemma HomoMorphism_Proper: Proper ((λ f g, ∀ a x, f a x = g a x) ==> iff) HomoMorphism.
proof: Proof. Proof with try apply _; intuition. intros x y E1. constructor; intros [? ? ? ?]; simpl in *. repeat constructor... intros ? ? E2. rewrite <-2!E1. rewrite E2... apply (Preservation_proper' x y E1 (σ o) (A_ops o) (B_ops o))... repeat constructor... intros ? ? E2. rewrite 2!E1. rewrite E2... assert (∀ (a : sorts σ) (x0 : A a), y a x0 = x a x0) as E2. symmetry. apply E1. apply (Preservation_proper' y x E2 (σ o) (A_ops o) (B_ops o))... Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra