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 list_permut_nil; setoid_rewrite H2; auto]. apply dickson_aux3; trivial. Qed.
imports: Relations List Setoid closure more_list Multiset list_permut