summaryrefslogtreecommitdiff
path: root/Nominal/Equivariance.lean
AgeCommit message (Collapse)Author
2025-10-26finish name abstraction proofsHannes Schulze
2025-10-25start working on alpha equivalence proofsHannes Schulze
2025-10-24use simp only everywhere except for last goalHannes Schulze
2025-10-24show properties for freshness quantifier based on equivariant relationsHannes Schulze
2025-10-24proof sketch for proving different AlphaEq characterizationsHannes Schulze
2025-10-23add forgetful functorsHannes Schulze
2025-10-23add equivariant instancesHannes Schulze
2025-10-23define equivarianceHannes Schulze