proposition: Theorem restrict_nth_default: forall l n m, m <= n -> nth n (restrict m l) o = o.
proof: Proof. intros l; elim l; simpl; auto; clear l. intros n m; case n; auto with arith. intros a l Rec n m; case m; auto; clear m. rewrite restrict_0. case n; simpl; auto. intros n1 _; generalize n1; elim (length l); clear n1; simpl; auto. intros n1; case n1; auto. intros n2 Rec1 n1; case n1; simpl; auto. intros n2; case n; simpl; auto with arith. intros H; contradict H; auto with arith. Qed.
imports: List ListAux UList OrderedList