proposition: Theorem empty_jump n s : empty s -> empty (jump n s).
proof: Proof. revert s; elim n; simpl; auto. intros n0 Rec s0; case s0; auto. intros a s1 H; apply Rec. intros p; case p; intros x y. generalize (H (Pos x (S y))); unfold get; simpl. rewrite <- plus_n_Sm; simpl; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia