proposition: Lemma remove_permut : forall l1 l2, permut l1 l2 -> forall a, match (remove eq_bool a l1) with | Some l => match (remove eq_bool a l2) with | Some l' => permut l l' | None => False end | None => remove eq_bool a l2 = None end.
proof: Proof. intros l1 l2 P a; generalize (remove_is_sound a l1) (remove_is_sound a l2). case (remove eq_bool a l1); case (remove eq_bool a l2). intros l l' P1 P2. rewrite (@permut_cons a a l' l). apply permut_trans with l2; trivial. apply permut_trans with l1; trivial. apply permut_sym; trivial. reflexivity. intros l P' a_not_in_l2; apply a_not_in_l2. rewrite <- (mem_permut_mem a P). rewrite (mem_permut_mem a P'); left; reflexivity. intros l a_not_in_l1 P'; assert False; [idtac | contradiction]. apply a_not_in_l1. rewrite (mem_permut_mem a P). rewrite (mem_permut_mem a P'); left; reflexivity. intros; apply eq_refl. Defined.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)