feat(LambdaCalculus/Named/Untyped): Alpha equivalence equalities - #741

Open

chris-anto-froeschl wants to merge 12 commits into

leanprover:mainfrom

chris-anto-froeschl:alpha-equivalence-equalities

Commits on Jun 1, 2026

Commits on Jun 8, 2026

solves alphaEquiv_iff_alphaEquivPFresh while adding necessary swap property helper lemmas, updates references.bib to include alpha equivalence definition sources
chris-anto-froeschl
committed

Commits on Jun 27, 2026

converges theorem 4.1 much closer to how the paper proof is structured, introduces agreement sets
chris-anto-froeschl
committed

Commits on Jul 21, 2026

switches to mathlibs Equiv.swap to build coherent picture wrt permutations
chris-anto-froeschl
committed

Commits on Jul 22, 2026