proposition: Lemma mult_irrefl : transitive _ R -> (forall a, ~ R a a) -> forall l, trans_clos (multiset_extension_step R) l l -> False.
proof: Proof. intros trans_R irrefl_R l l_lt_l. rewrite (app_nil_end l) in l_lt_l. assert (nil_lt_nil := remove_context_trans_clos_multiset_extension_step_app1 trans_R irrefl_R nil nil l l_lt_l). clear l l_lt_l. assert (H : forall l1 l2, trans_clos (multiset_extension_step R) l1 l2 -> l2 = nil -> False). intros l1 l2 T; induction T as [k1 k2 H | k1 k2 k3 H1 H2]; intros; subst. inversion H as [l1 l2 l la a la_lt_a P1 P2]; subst. generalize (permut_length P2); simpl; discriminate. apply IHH2; apply eq_refl. apply (H _ _ nil_lt_nil); apply eq_refl. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)