proposition: Lemma combine_jump : forall A n (l1 l2: list A), combine (jump n l1) (jump n l2) = jump n (combine l1 l2).
proof: Proof. intros A n l1;functional induction (jump n l1);simpl;intros l2. rewrite IHl0;rewrite IHl;rewrite combine_tail;reflexivity. rewrite IHl0;rewrite IHl;reflexivity. rewrite combine_tail;reflexivity. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)