proposition: Lemma remove_equiv_permut_2: forall l1 l2 l2', permut l2 l2' -> (fst (remove_equiv eq_bool l1 l2) = fst (remove_equiv eq_bool l1 l2') /\ permut (snd (remove_equiv eq_bool l1 l2)) (snd (remove_equiv eq_bool l1 l2'))).
proof: Proof. fix remove_equiv_permut_2 1. intros [ | a1 l1] l2 l2' P. simpl; split; [apply eq_refl | trivial]. simpl; generalize (remove_permut P a1). case_eq (remove eq_bool a1 l2); [intro k2 | idtac]; intro H2. case_eq (remove eq_bool a1 l2'); [intro k2' | idtac]; intro H2'. intro P'; assert (H := remove_equiv_permut_2 l1 _ _ P'); case H; intros H' H''; split; trivial. intro; apply False_rect; trivial. intro H2'; rewrite H2'. assert (H := remove_equiv_permut_2 l1 _ _ P); case H; intros H' H''; split. revert H'; case (remove_equiv eq_bool l1 l2); intros k1 k2; case (remove_equiv eq_bool l1 l2'); intros k1' k2'; simpl; intros; subst; trivial. revert H''; case (remove_equiv eq_bool l1 l2); intros k1 k2; case (remove_equiv eq_bool l1 l2'); intros k1' k2'; simpl; intros; subst; trivial. Defined.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)