proposition: Lemma remove_equiv_permut: forall l1 l1' l2 l2', permut l1 l1' -> permut l2 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' l2 l2' P1 P2. generalize (remove_equiv_permut_1 P1 l2) (remove_equiv_permut_2 l1' P2). case (remove_equiv eq_bool l1 l2); case (remove_equiv eq_bool l1' l2); case (remove_equiv eq_bool l1' l2'); simpl; intros u1 u2 u3 u4 u5 u6 [Q1 Q2] [Q3 Q4]; split. subst; assumption. apply permut_trans with u4; assumption. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)