proposition: Fact vec_map_ext f g n v : (forall x, in_vec x v -> f x = g x) -> @vec_map X Y f n v = vec_map g v.
proof: Proof. intros H. do 2 rewrite <- vec_in_map_vec_map_eq. apply vec_in_map_ext, H. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)