proposition: Lemma dickson_aux3 : forall R a, Acc R a -> forall m, Acc (multiset_extension_step R) m -> Acc (multiset_extension_step R) (a :: m).
proof: Proof. intros R a Acc_a; apply (Acc_iter (R:= R) (fun a => Acc R a -> forall m, Acc (multiset_extension_step R) m -> Acc (multiset_extension_step R) (a :: m))); trivial; clear a Acc_a; intros a H Acc_a m Acc_m; apply dickson_aux2; trivial; intros; apply H; trivial; apply Acc_inv with a; trivial. Qed.
imports: Relations List Setoid closure more_list Multiset list_permut