proposition: Lemma remove_equiv_nil_2 : forall l, remove_equiv eq_bool l nil = (l,nil).
proof: Proof. fix remove_equiv_nil_2 1. intros [ | a l]; simpl. apply eq_refl. rewrite remove_equiv_nil_2; apply eq_refl. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)