proposition: Lemma jump_combine : forall A n (l1 l2:list A), jump n (combine l1 l2) = combine (jump n l1) (jump n l2).
proof: Proof. induction n; simpl. intros l1 l2. do 2 rewrite <- IHn. do 2 f_equal. destruct l1;destruct l2;simpl;try reflexivity. destruct l1;simpl; reflexivity. intros l1 l2. do 2 rewrite <- IHn. do 2 f_equal. intros l1 l2. destruct l1;destruct l2;simpl;try reflexivity. destruct l1;simpl; reflexivity. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)