proposition: Lemma Mjump_add M i j l : M @@ (jump (i + j) l) = M @@ (jump j (jump i l)).
proof: Proof. apply Mphi_morph. intros. now rewrite <- jump_add, Pos.add_comm. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory