proposition: Lemma dickson_aux1 : forall (R : relation elt) a, (forall b, R b a -> forall m, Acc (multiset_extension_step R) m -> Acc (multiset_extension_step R) (b :: m)) -> forall m, Acc (multiset_extension_step R) m -> (forall m', (multiset_extension_step R) m' m -> Acc (multiset_extension_step R) (a :: m')) -> Acc (multiset_extension_step R) (a :: m).
proof: Proof. intros R a IH2_a m Acc_m IHa_M; apply Acc_intro; intros n H; elim (two_cases H); clear H. intros [n' [P M]]; refine (list_permut_acc P _); apply IHa_M; trivial. intros [k [M P]]; refine (list_permut_acc P _); clear P; induction k; trivial; simpl; apply IH2_a. apply M; left; trivial. apply IHk; intros; apply M; right; trivial. Qed.
imports: Relations List Setoid closure more_list Multiset list_permut