proposition: Lemma fset_eq_in X Y : X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
proof: Proof. setoid_rewrite <-to_listset_preserves_in. split. intros E. change (to_listset X = to_listset Y). now apply sm_proper. intros. now apply (injective (to_listset)). 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