proposition: Lemma wlt_len_gen : forall (w1 w2:list nat) (a:nat), (lt (length w1) (length (cons (S a) w2))) -> (wlt w1 (cons (S a) w2)).
proof: Proof. induction w1. intros. apply wlt_nil. intros. destruct a. apply wlt_0_w. apply IHw1. apply Nat.lt_trans with (m:=(length (cons 0 w1))). auto with arith. assumption. apply wlt_len. auto with arith. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef