proposition: Lemma map_ext_in A B: forall (f g:A->B) n (v : t A n), (forall a, In a v -> f a = g a) -> map f v = map g v.
proof: Proof. intros f g n v H; induction v as [|? ? v IHv]. - reflexivity. - cbn. now f_equal; [|apply IHv; intros ??]; apply H; [left|right]. Qed.
imports: VectorDef PeanoNat Eqdep_dec