proposition: Lemma listset_add_raw_cons l x : x :: l = listset_add_raw x l.
proof: Proof. induction l; simpl; try reflexivity. case (decide_rel _); intros E. now rewrite E, equivlistA_double_head. now rewrite equivlistA_permute_heads, IHl. 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