proposition: Lemma list_permut_trans_clos_multiset_extension_step_1 : forall R l1 l2 l, permut l1 l2 -> (trans_clos (multiset_extension_step R)) l1 l -> (trans_clos (multiset_extension_step R)) l2 l.
proof: Proof. intros R l1 l1' l P H; induction H as [ l1 l2 H | l1 l2 l3 H1 H2 H3]. apply t_step; apply list_permut_multiset_extension_step_1 with l1; trivial. apply t_trans with l2; trivial; apply list_permut_multiset_extension_step_1 with l1; trivial. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)