proposition: Lemma fset_join_singletons_eq_l x y : {{ x ; y }} = {{ x }} ↔ x = y.
proof: Proof. split. intros E1. apply stable; intros E2. assert (fset_extend (F x y) {{ x ; y }} ≠ fset_extend (F x y) {{ x }}) as E3. rewrite preserves_join, <-!(fset_extend_correct_applied (F x y)). unfold F. do 2 (case (decide _)); intuition try discriminate; auto. destruct E3. now rewrite E1. intros E. now rewrite E, fset_join_singletons. 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