proposition: Lemma jump_pred_double : forall i l, jump (Pos.pred_double i) (tl l) = jump i (jump i l).
proof: Proof. intro i;induction i as [i IHi|i IHi|];intros;simpl. - now rewrite !jump_tl. - now rewrite IHi, <- 2 jump_tl, IHi. - trivial. Qed.
imports: BinPos List