proposition: Fact vec_in_map_ext n v f g : (forall x Hx, @f x Hx = @g x Hx) -> @vec_in_map n v f = vec_in_map v g.
proof: Proof. revert f g; induction v; simpl; intros; f_equal; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)