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