proposition: Lemma dickson : forall R, well_founded R -> well_founded (multiset_extension_step R).
proof: Proof. intros R Wf_R; unfold well_founded in *; intros m; induction m as [ | a m]. apply Acc_intro; intros m H; inversion_clear H; absurd (a :: l = nil). discriminate. apply (permut_nil (R := eq_A)). apply permut_sym; trivial. apply dickson_aux3; trivial. Defined.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)