proposition: Lemma wf_length : well_founded o_length.
proof: Proof. unfold well_founded, o_length. intros [l f]; apply Acc_intro. generalize (length l); clear f l. intro n; induction n as [ | n]. intros [y f] Abs; absurd (length y < 0); auto with arith. intros [y f] Sy; inversion Sy; subst. apply Acc_intro; intros x Sx; apply IHn; trivial. apply IHn; trivial. Defined.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)