proposition: Lemma jump_simpl p l x : jump p l x = match p with | xH => tail l x | xO p => jump p (jump p l) x | xI p => jump p (jump p (tail l)) x end.
proof: Proof. destruct p; unfold tail; rewrite <- ?jump_add; f_equal; now rewrite Pos.add_diag. Qed.
imports: BinInt List