fact: Parameter remove_equiv_is_complete : forall l1 l2 l l1' l2', permut l1 (l ++ l1') -> permut l2 (l ++ l2') -> (forall x, mem eq_A x l1' -> mem eq_A x l2' -> False) -> (permut (fst (remove_equiv eq_bool l1 l2)) l1' /\ permut (snd (remove_equiv eq_bool l1 l2)) l2').
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)