proposition: Lemma wf_lessP3 : well_founded lessP3.
proof: Proof. red in |- *. cut (forall (m : nat) a, sizel3 a < m -> Acc lessP3 a). intros H' a. apply H' with (m := S (sizel3 a)); auto. intros m; elim m; clear m. intros a H; inversion H. intros p H' a H'0; apply Acc_intro. intros y H'1; apply H'. unfold lessP in H'1; apply Nat.lt_le_trans with (sizel3 a); auto with arith. Qed.
imports: Coq(Arith Compare_dec)