proposition: Lemma Acc_mwlt : forall (A:Set) (m: A -> list nat), forall (x:A), (Acc (fun x1 x2 => (wlt (m x1) (m x2))) x).
proof: Proof. intros. apply Acc_wlt_eq with (w:=(m x)). trivial. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef