fact: Parameter list_permut_flatten : forall f l1 l2, permut l1 l2 -> permut (flatten f l1) (flatten f l2).
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)