proposition: Theorem length_take_small: forall i l, length l <= i -> length (take i l) = length l.
proof: Proof. intros i l; generalize i; elim l; clear i l; simpl; auto. intros; rewrite take_nil; auto. intros a l Rec i; case i; simpl; auto with arith. Qed.
imports: List ListAux UList OrderedList