Nominal sets

The Gabbay–Pitts theory of names and symmetry, over a countable set of atoms: finite permutations, nominal sets (finitely-supported permutation actions), freshness and the И (new) quantifier, support, and name abstraction. This layer depends only on mathlib.

References

• Pitts, Nominal Sets: Names and Symmetry in Computer Science, Cambridge University Press, 2013.
• Larsen and Schürmann, Nominal State-Separating Proofs, IACR ePrint 2025/598 — the SSProve Nominal/ layer this development ports.