proposition: Lemma fset_extend_correct_applied `{BoundedJoinSemiLattice B} (f : A → B) `{!Setoid_Morphism f} x : f x = fset_extend f {{ x }}.
proof: Proof. now apply fset_extend_correct. 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