chore: cleanup of Cslib.Languages.LambdaCalculus.LocallyNameless.*

[chenson2018]

With the somewhat recent change to allow passing arbitrary expressions to grind and other improvements, some cleanup of locally nameless lambda calculus is possible.

[chenson2018]

!radar

[leanprover-radar]

Benchmark results for 384d1c6 against ab28b63 are in! @chenson2018

Large changes (1🟥)

• 🟥 build//instructions: +21.3G (+1.2%)

[chenson2018]

!radar

[leanprover-radar]

Benchmark results for 5042047 against ab28b63 are in! @chenson2018

Large changes (1🟥)

• 🟥 build//instructions: +26.1G (+1.5%)

[chenson2018]

!radar

[leanprover-radar]

Benchmark results for 890cc9f against ab28b63 are in! @chenson2018

Medium changes (1🟥)

• 🟥 build//instructions: +14.0G (+0.8%)

[chenson2018]

Sorry about the benchmarking noise, I made several wrong guesses before I tracked down the main issues. While the overall build is +0.8% I think this is an acceptable tradeoff for some nicer proofs and a +92 −161 diff. (Some files did get faster, so maybe we're close to the margin of error.)