proposition: Lemma listset_extend_raw_permute (l k : list A) : PermutationA (=) l k → listset_extend_raw f l = listset_extend_raw f k.
proof: Proof. induction 1; simpl. reflexivity. apply sg_op_proper. now apply sm_proper. easy. now rewrite !associativity, (commutativity (f _)). etransitivity; eassumption. Qed.
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