1 files changed, 47 insertions, 2 deletions
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 8475a21..368d266 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -195,11 +195,56 @@ namespace Equivariance
 
 variable {X : Type} [NominalSet 𝔸 X] {R: Rel 𝔸 X} {x : X}
 
+-- We continue with a circular implication chain argument to show these equivalences.
+
+private lemma for_fresh_iff₁ : EquivariantRelation 𝔸 R → (И a, R a x) → (∃ a, a # x ∧ R a x) := by
+  intro hequi h
+  have hinf : ({a | R a x} \ NominalSet.supp 𝔸 x).Infinite := Set.Infinite.diff h (NominalSet.supp_finite 𝔸)
+  obtain ⟨a, ha⟩ := hinf.nonempty
+  simp at ha
+  use a; exact ha.symm
+
+private lemma for_fresh_iff₂ : EquivariantRelation 𝔸 R → (∃ a, a # x ∧ R a x) → (∀ a, a # x → R a x) := by
+  intro hequi h
+  obtain ⟨a, ⟨hfresha, ha⟩⟩ := h
+  intro b hfreshb
+  have hmem := hequi a x ⸨a, b⸩ ha
+  rw [PermSet.atom_swap, Equiv.swap_apply_left] at hmem
+  rw [NominalSet.fresh_swap_fix 𝔸 hfresha hfreshb] at hmem
+  exact hmem
+
+private lemma for_fresh_iff₃ : EquivariantRelation 𝔸 R → (∀ a, a # x → R a x) → (И a, R a x) := by
+  intro hequi h
+  have hsub : {a : 𝔸 | R a x}ᶜ ⊆ NominalSet.supp 𝔸 x := by
+    rw [Set.compl_subset_comm]
+    intro a ha
+    rw [Set.mem_compl_iff] at ha
+    exact h a ha
+  simp [NominalSet.ForFresh]
+  apply Set.infinite_of_finite_compl
+  apply Set.Finite.subset (NominalSet.supp_finite 𝔸) hsub
+
 /-- 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
+lemma for_fresh_iff_exists : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∃ a, a # x ∧ R a x)) := by
+  intro hequi; constructor
+  · intro h
+    apply for_fresh_iff₁ 𝔸 hequi
+    exact h
+  · intro h
+    apply for_fresh_iff₃ 𝔸 hequi
+    apply for_fresh_iff₂ 𝔸 hequi
+    exact h
 
 /-- 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
+lemma for_fresh_iff_all : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∀ a, a # x → R a x)) := by
+  intro hequi; constructor
+  · intro h
+    apply for_fresh_iff₂ 𝔸 hequi
+    apply for_fresh_iff₁ 𝔸 hequi
+    exact h
+  · intro h
+    apply for_fresh_iff₃ 𝔸 hequi
+    exact h
 
 end Equivariance