proposition: Lemma fset_map_id `{FSet A} : fset_map id = id.
proof: Proof. pose proof (fset_car_setoid A). symmetry. apply (fset_map_unique id id). 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