proposition: Lemma image_proper: ∀ s (x0 x' : B s), x0 = x' → iffT (image s x0) (image s x').
proof: Proof. intros ??? E. split; intros [v ?]; exists v; rewrite E in *; assumption. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebraT MathClasses.misc.util