proposition: Lemma fset_extend_unique_applied `{Equiv B} `{Join B} `{Bottom B} (f : A → B) `{!Setoid_Morphism f} (h : set_type A → B) `{!BoundedJoinSemiLattice_Morphism (h : set_type A → B)} : (∀ x, f x = h {{ x }}) → ∀ x, h x = fset_extend f x.
proof: Proof. intros. apply setoids.ext_equiv_applied, (fset_extend_unique _ _). now apply setoids.ext_equiv_applied_iff. 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