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