proposition: Theorem restrict_update: forall n l, S n <= length l -> restrict (S n) l = subst n (nth 0 (jump n l) o) (restrict n l).
proof: Proof. intros n l; generalize n; elim l; auto with datatypes; clear n l. intros n H; contradict H; auto with arith. intros a l1 Rec n; case n; auto; clear n. simpl length; intros n H; simpl; f_equal; auto with arith. Qed.
imports: List ListAux UList OrderedList