proposition: Lemma Pjump_pred_double P p l : P @ (jump (Pos.pred_double p) (tail l)) = P @ (jump (xO p) l).
proof: Proof. apply env_morph. intros. rewrite jump_pred_double. now jump_simpl. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory