proposition: Lemma remove_equiv_permut_1 : forall l1 l1', permut l1 l1' -> forall l2, (permut (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. intros l1 l1' P1 l2; generalize (remove_equiv_is_sound l1 l2) (remove_equiv_is_sound l1' l2). case_eq (remove_equiv eq_bool l1 l2); intros k1 k2 H1; intros [l [Q1 [Q2 H]]]. case_eq (remove_equiv eq_bool l1' l2); intros k1' k2' H1'; intros [l' [Q1' [Q2' H']]]. simpl; assert (Q1'' : permut l1 (l' ++ k1')). apply permut_trans with l1'; trivial. assert (R := @remove_equiv_is_complete l1 l2 l' k1' k2' Q1'' Q2' H'); rewrite H1 in R. revert R; intros [R1 R2]; split; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)