fact: Parameter remove_equiv_is_sound: forall l1 l2, match remove_equiv eq_bool l1 l2 with | (l1', l2') => exists l, permut l1 (l ++ l1') /\ permut l2 (l ++ l2') /\ (forall x, mem eq_A x l1' -> mem eq_A x l2' -> False) end.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)