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