proposition: Lemma jump_pred_double i l x : jump (Pos.pred_double i) (tail l) x = jump i (jump i l) x.
proof: Proof. unfold tail. rewrite <- !jump_add. f_equal. now rewrite Pos.add_1_r, Pos.succ_pred_double, Pos.add_diag. Qed.
imports: BinInt List