proposition: Lemma Acc_wlt_pad_Acc_wlt : forall (w:(list nat)), (Acc wlt_pad w) -> (Acc wlt w).
proof: Proof. intros. elim H. intros w' H0 H1. apply Acc_intro. intros w'' H2. elim (nat_compare_case (length w'') (length w')). intro. apply Acc_wlt_zs_Acc_wlt with (n:=(dist w' w'')). apply H1. apply wlt_wlt_pad_zs; assumption. intro. elim H3. intro. apply H1. apply wlt_wlt_pad; assumption. intro. elim (wlt_gt_length w'' w' H2 H4). intros a H5. elim H5. intro w0. intro. decompose [and] H6. rewrite H7. apply Acc_wlt_Acc_wlt_zs. apply H1. apply wlt_wlt_pad; assumption. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef