fact: Parameter remove_is_sound : forall x l, match remove eq_bool x l with | None => ~mem eq_A x l | Some l' => permut l (x :: l') end.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)