proposition: Lemma remove_context_trans_clos_multiset_extension_step_app1 : forall R, transitive _ R -> (forall a, ~R a a) -> forall l1 l2 l, trans_clos (multiset_extension_step R) (l ++ l1) (l ++ l2) -> trans_clos (multiset_extension_step R) l1 l2.
proof: Proof. intros R trans_R irrefl_R l1 l2 l; generalize l1 l2; clear l1 l2; induction l as [ | a l]; trivial. intros l1 l2 H; apply IHl; apply context_trans_clos_multiset_extension_step_cons with a; trivial. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)