proposition: Lemma Forall_map A B: forall (P : B -> Prop) (f : A -> B) n (v : t A n), Forall P (map f v) <-> Forall (fun x => P (f x)) v.
proof: Proof. intros P f n v. induction v as [|a n v IH]. - split; constructor. - cbn. now rewrite !Forall_cons_iff, IH. Qed.
imports: VectorDef PeanoNat Eqdep_dec