proposition: Lemma singleton_correct_alt : At_to_Bt⁻¹ ∘ singleton = singleton ∘ A_to_B⁻¹.
proof: Proof. pose proof (injective_mor A_to_B). pose proof (injective_mor At_to_Bt). apply (jections.injective_compose_cancel At_to_Bt). rewrite <-!compose_assoc. rewrite (surjective At_to_Bt), singleton_correct. rewrite compose_assoc, (surjective A_to_B). rewrite compose_id_left, compose_id_right. now apply setoids.ext_equiv_refl. Qed.
imports: MathClasses.theory.lattices MathClasses.varieties.monoids MathClasses.implementations.bool MathClasses.implementations.list_finite_set MathClasses.orders.lattices MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders