proposition: Lemma 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).
proof: Proof. intros R l1 l2 l H; induction H. apply t_step; apply context_multiset_extension_step_app1; trivial. apply t_trans with (l ++ y); trivial. apply context_multiset_extension_step_app1; trivial. Qed.
imports: Relations List Setoid closure more_list Multiset list_permut