proposition: Lemma fold_right_shiftin A B: forall (f : A -> B -> B) a b n (v : t A n), fold_right f (shiftin b v) a = fold_right f v (f b a).
proof: Proof. intros f a b n v. induction v as [|c n v IH]. - reflexivity. - cbn. apply f_equal, IH. Qed.
imports: VectorDef PeanoNat Eqdep_dec