fact: Fixpoint listset_extend_raw `{Bottom B} `{Join B} (f : A → B) (l : list A) : B := match l with | [] => ⊥ | x :: l => f x ⊔ listset_extend_raw f l end.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.implementations.list MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders MathClasses.theory.lattices MathClasses.orders.lattices