proposition: Lemma ext_equiv_applied_iff `{Equiv A} `{Equiv B} `{!Setoid_Morphism (f : A → B)} `{!Setoid_Morphism (g : A → B)} : f = g ↔ ∀ x, f x = g x.
proof: Proof. pose proof (setoidmor_a f). pose proof (setoidmor_b f). split; intros E1. now apply ext_equiv_applied. intros x y E2. now rewrite E2. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.products