feat: FullEta.step_lc_l

[lengyijun]

This PR adds a missing lemma to the FullEta development in the locally nameless untyped λ‑calculus:
a proof that the source term of a single‑step η‑reduction is locally closed. It also moves the definition of LcAt earlier to avoid some duplication of proofs about LC.

New Lemmas

FullEta.step_lc_l : Proves that the left side of an η-reduction step (M ⭢ηᶠ M') is locally closed.
Uses induction on the reduction step and the grind tactic.

lcAt_openRec_above_lcAt : Shows that opening a term at a higher index than its locally closed level leaves it unchanged.

Refactored Lemmas

open_lc : Simplified proof using lcAt_openRec_above_lcAt and lcAt_iff_LC.

PR description is generated by AI

[lengyijun]

Compared to FullBeta.step_lc_l, FullEta.step_lc_l requires HasFresh

[lengyijun]

Fail to find theorem N.LC -> N.openRec i M = N, so I prove it with LcAt

[chenson2018]

I took the liberty of moving around imports so that any generalizations of LcAt don't get duplicated.

[chenson2018]

The PR description is very large proportional to the change, maybe just the first line is needed? If AI was used, it is our policy is that this is disclosed when opening the PR.

[lengyijun]

If AI was used, it is our policy is that this is disclosed when opening the PR.

Not mentioned in CONTRIBUTING.md

[chenson2018]

If AI was used, it is our policy is that this is disclosed when opening the PR.

Not mentioned in CONTRIBUTING.md

This has been a policy for some time in alignment with Mathlib, but you are correct that it was not documented. I have opened a PR to correct this oversight. Thank you for complying in the meantime! I made an additional small edit to include the change I made to the import structure.