proposition: Theorem length_jump: forall i s, i <= length s -> length s = length (jump i s) + i.
proof: Proof. intros i. induction i; auto; intros s H; simpl. - destruct s. + inversion H. + simpl. rewrite <- plus_n_Sm; auto with arith. Qed.
imports: List ListAux UList OrderedList