proposition: Lemma Acc_wlt_eq : forall (A:Set) (m: A -> list nat) (w:list nat) (x:A) , w = (m x) -> (Acc (fun x1 x2 : A => wlt (m x1) (m x2)) x).
proof: Proof. induction w using wlt_wf_ind. intros. apply Acc_intro. intros. apply H with (w2:=(m y)). rewrite H0. assumption. trivial. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef