proposition: Lemma Acc_wlt_pad : forall (w:(list nat)), (Acc wlt_pad w).
proof: Proof. induction w using list_length_ind. apply Acc_wlt_pad_nil. apply Acc_wlt_pad_ind with (n:=n); assumption. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef