From 96164bc58172cbec5579e8bf38933dfb5cc51381 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Fri, 24 Oct 2025 00:54:44 +0200
Subject: proof sketch for proving different AlphaEq characterizations

---
 Nominal/Equivariance.lean | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'Nominal/Equivariance.lean')

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index ac50519..8475a21 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -184,6 +184,27 @@ lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸
 
 end Nominal
 
+/-!
+## Freshness
+
+For propositions of the form `И a, a R x`, where `R` is an equivariant relation, we do not have to differentiate between "for any fresh a" and "for all fresh a".
+-/
+section Freshness
+
+namespace Equivariance
+
+variable {X : Type} [NominalSet 𝔸 X] {R: Rel 𝔸 X} {x : X}
+
+/-- The quantifier in `И a, a R x` is equivalent to "for any fresh `a`". -/
+lemma for_fresh_iff_exists : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∃ a, a # x ∧ R a x)) := by sorry
+
+/-- The quantifier in `И a, a R x` is equivalent to "for all fresh `a`". -/
+lemma for_fresh_iff_all : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∀ a, a # x → R a x)) := by sorry
+
+end Equivariance
+
+end Freshness
+
 /-!
 ## Bundled Functions
 
-- 
cgit v1.3.1