proposition: Lemma Pjump_add P i j l : P @ (jump (i + j) l) = P @ (jump j (jump i l)).
proof: Proof. apply env_morph. intros. rewrite <- jump_add. f_equal. apply Pos.add_comm. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory