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