proposition: Lemma jump_nil : forall p, jump p (@nil Z) = nil .
proof: Proof. induction p;simpl. do 2 rewrite IHp;reflexivity. do 2 rewrite IHp;reflexivity. reflexivity. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)