proposition: Lemma 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.
proof: Proof. intros x l; generalize (in_remove eq_A eq_bool eq_bool_ok x l); case (remove eq_bool x l); [ intros k [x' [l' [l'' [x_eq_x' [H1 H2]]]]] | idtac]. injection H2; clear H2; intros; subst. apply permut_sym; rewrite <- permut_cons_inside; auto. intro; assumption. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)