proposition: Theorem restrict_nth: forall l n m, n < m -> nth n (restrict m l) o = nth n l o.
proof: Proof. intros l; elim l; simpl; auto; clear l. intros a l Rec n m; case m; auto; clear m. intros H; contradict H; auto with arith. intros m; case n; clear n; auto. intros n; simpl; auto with arith. Qed.
imports: List ListAux UList OrderedList