proposition: Lemma map_rev A B: forall (f : A -> B) n (v : t A n), map f (rev v) = rev (map f v).
proof: Proof. intros f n v. induction v as [|a n v IH]; cbn. - now rewrite !rev_nil. - now rewrite !rev_cons, map_shiftin, IH. Qed.
imports: VectorDef PeanoNat Eqdep_dec