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