proposition: Lemma dickson_strong : forall R l, (forall a, In a l -> Acc R a) -> Acc (multiset_extension_step R) l.
proof: Proof. intros R m; induction m as [ | a m]. intros _; apply Acc_intro; intros m H; inversion_clear H; absurd (a :: l = nil). discriminate. apply (permut_nil (R := eq_A)). apply permut_sym; trivial. intros; apply dickson_aux3. apply H; left; trivial. apply IHm; intros; apply H; right; trivial. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)