proposition: Theorem restrict_length: forall n l, length (restrict n l) = (length l).
proof: Proof. intros n l; generalize n; elim l; simpl; auto with datatypes; clear n l. intros a l Rec n; case n; simpl; auto. Qed.
imports: List ListAux UList OrderedList