fact: Parameter 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')).
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)