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