Liberating Semi-Automated PL Proofs from Binder Bookkeeping