proposition: Lemma jump_in : forall A n l (x:A), In x (jump n l) -> @In A x l.
proof: Proof. intros a n l;functional induction (jump n l). intros;apply tail_in;eauto. eauto. intros;apply tail_in;auto. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)