proposition: Theorem restrict_all: forall n l, length l <= n -> restrict n l = l.
proof: Proof. intros n l; generalize n; elim l; simpl; auto with datatypes; clear n l. intros a l Rec n; case n; auto with arith. intros H; contradict H; auto with arith. intros n1 H; f_equal; auto with arith. Qed.
imports: List ListAux UList OrderedList