fact: Parameter flatten_app : forall f l1 l2, flatten f (l1 ++ l2) = (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)