Commit 2025-11-06 20:50 3bfbe167

fix(push_neg): preserve binder names (#31212) This PR fixes the push_neg tactic so that it preserves binder names when pushing through Exists. It was previously picking up the x name from ∃ x, s x, so spelling it as Exists s fixes the problem.