fact: Parameter list_permut_multiset_extension_step_2 : forall R l1 l2 l, permut l1 l2 -> multiset_extension_step R l l1 -> multiset_extension_step R l l2.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)