proposition: Lemma Preservation_proper' (f g: ∀ a, A a → B a) `{∀ a, Setoid (A a)} `{∀ b, Setoid (B b)} `{∀ a, Setoid_Morphism (@f a)}: (∀ a (x: A a), f a x = g a x) → ∀ (n: OpType) x y, Proper (=) x → Proper (=) y → @Preservation f n x y → @Preservation g n x y.
proof: Proof. induction n. simpl. intros ? ? ? ? E. rewrite <-E. symmetry. intuition. simpl. intros a b E1 E2 E3 z. apply IHn. apply E1. reflexivity. apply E2. reflexivity. assert (b (g _ z) = b (f _ z)) as E4. apply E2. symmetry. apply H2. now apply (Preservation_proper'' f n (a z) (a z) eq_refl _ _ E4). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra