proposition: Theorem well_founded_length : forall A, well_founded (o_length (A := A)).
proof: Proof. intro A; assert (Acc_nil : Acc (o_length (A:=A)) (@nil A)). apply Acc_intro; intros l H; absurd (o_length l nil); trivial; unfold o_length; simpl; auto with arith. unfold well_founded, o_length; intros l; pattern l; apply list_rec2; clear l; induction n; intro l; destruct l; intros H; trivial. simpl in H; absurd (S (length l) <= 0); trivial; auto with arith. apply Acc_intro; intros l' H'; apply IHn; apply Nat.le_trans with (length l); simpl in H; simpl in H'; auto with arith. Defined.
imports: Coq(List Arith)