proposition: Lemma wlt_wf_ind : forall (P: (list nat) -> Prop), (forall (w1:list nat), (forall (w2:list nat), (wlt w2 w1) -> P w2) -> P w1) -> forall (w:list nat), P w.
proof: Proof. intros. apply well_founded_ind with (R:=wlt). unfold well_founded. apply Acc_wlt. intros. apply H. assumption. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef