proposition: Lemma Acc_wlt_zs_Acc_wlt : forall (n:nat) (w:(list nat)), (Acc wlt (app (zs n) w)) -> (Acc wlt w).
proof: Proof. intros. apply Acc_intro. intros w' H0. apply H. apply wlt_wlt_zs_right. assumption. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef