cleanup

2 files changed, 199 insertions, 129 deletions

diff --git a/Nominal/NameRestriction/Finsupp.lean b/Nominal/NameRestriction/Finsupp.lean
index 3059bba..4311bee 100644
--- a/Nominal/NameRestriction/Finsupp.lean
+++ b/Nominal/NameRestriction/Finsupp.lean
@@ -64,6 +64,19 @@ instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X → Y)
 abbrev FinsuppFunction (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] : Type :=
   Finsupp 𝔸 (X → Y)
 
+lemma FinsuppFunction.supp_image {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] (f : PermSet.FinsuppFunction 𝔸 X Y) :
+    ∀ x, PermSet.HasSupport 𝔸 (f.val x) (NominalSet.supp 𝔸 f ∪ NominalSet.supp 𝔸 x) := by
+  intro x π hπ
+  have hπ₁ : π ∈ PermSet.fix 𝔸 (NominalSet.supp 𝔸 f) := by
+    apply PermSet.fix_antitone_mem 𝔸 hπ; exact Set.subset_union_left
+  have hπ₂ : π ∈ PermSet.fix 𝔸 (NominalSet.supp 𝔸 x) := by
+    apply PermSet.fix_antitone_mem 𝔸 hπ; exact Set.subset_union_right
+  suffices (π • f).val (π • x) = f.val x by
+    simp at this
+    exact this
+  rw [show π • f = f from NominalSet.supp_is_support 𝔸 hπ₁]
+  rw [show π • x = x from NominalSet.supp_is_support 𝔸 hπ₂]
+
 variable (X Y : Type) [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
 
 namespace Finsupp
diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean
index 6195099..d09bebd 100644
--- a/Nominal/NameRestriction/Model.lean
+++ b/Nominal/NameRestriction/Model.lean
@@ -208,15 +208,18 @@ end BaseModel
 
 -- Step Model: \bar{M₁} X
 
-def Req1 {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :=
-  -- Support for individual atoms may only additionally add that atom
-  ∀ a, PermSet.HasSupport 𝔸 (f.val a) (NominalSet.supp 𝔸 f ∪ {a})
+lemma supp_image {X : Type} [NominalSet 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :
+    ∀ a, PermSet.HasSupport 𝔸 (f.val a) (NominalSet.supp 𝔸 f ∪ {a}) := by
+  intro a
+  have := PermSet.FinsuppFunction.supp_image 𝔸 f a
+  rw [NominalSet.supp_atom] at this
+  exact this
 
-lemma Req1.choose_restriction
+lemma choose_restriction'
     {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :
-    Req1 𝔸 f → ∀ (a b c d : 𝔸), c # f → d # f → c ≠ a → d ≠ a → c ≠ b → d ≠ b →
+    ∀ (a b c d : 𝔸), c # f → d # f → c ≠ a → d ≠ a → c ≠ b → d ≠ b →
       (c \ (⸨a, c⸩ • f).val b) = (d \ (⸨a, d⸩ • f).val b) := by
-  intro hreq a b c d hcfresh hdfresh hca hda hcb hdb
+  intro a b c d hcfresh hdfresh hca hda hcb hdb
   by_cases heq : b = a
   · nth_rw 1 [← show ⸨c, d⸩ • f = f from NominalSet.fresh_swap_fix 𝔸 hcfresh hdfresh]
     simp only [heq, PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv,
@@ -242,7 +245,7 @@ lemma Req1.choose_restriction
       suffices c ∉ NominalSet.supp 𝔸 (⟪a⟫ f.val d) by contradiction
       suffices c ∉ NominalSet.supp 𝔸 (f.val d) by simp [this]
       intro hc
-      have h := NominalSet.support_subset_supp 𝔸 (hreq d) (by simp [NominalSet.supp_finite])
+      have h := NominalSet.support_subset_supp 𝔸 (supp_image 𝔸 f d) (by simp [NominalSet.supp_finite])
       specialize h hc
       simp only [Set.union_singleton, Set.mem_insert_iff] at h
       cases h
@@ -263,7 +266,7 @@ lemma Req1.choose_restriction
       · rw [NameAbstraction.fresh]; right; rfl
       · rw [NameAbstraction.fresh]; left
         rw [NominalSet.IsFresh]; intro hcontra
-        have h := NominalSet.support_subset_supp 𝔸 (hreq b) (by simp [NominalSet.supp_finite]) hcontra
+        have h := NominalSet.support_subset_supp 𝔸 (supp_image 𝔸 f b) (by simp [NominalSet.supp_finite]) hcontra
         simp only [Set.union_singleton, Set.mem_insert_iff] at h
         cases h <;> contradiction]
     rw [show ⸨a,d⸩ • ⟪a⟫ f.val b = ⟪a⟫ f.val b by
@@ -271,7 +274,7 @@ lemma Req1.choose_restriction
       · rw [NameAbstraction.fresh]; right; rfl
       · rw [NameAbstraction.fresh]; left
         rw [NominalSet.IsFresh]; intro hcontra
-        have h := NominalSet.support_subset_supp 𝔸 (hreq b) (by simp [NominalSet.supp_finite]) hcontra
+        have h := NominalSet.support_subset_supp 𝔸 (supp_image 𝔸 f b) (by simp [NominalSet.supp_finite]) hcontra
         simp only [Set.union_singleton, Set.mem_insert_iff] at h
         cases h <;> contradiction]
 
@@ -280,7 +283,7 @@ def Req2 {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.F
   ∀ a c, c # f → c ≠ a → f.val a = f.val a ∨[𝔸] (c \ (⸨a, c⸩ • f).val a)
 
 def permissibleFunctions (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] :=
-  { f : PermSet.FinsuppFunction 𝔸 𝔸 X | Req1 𝔸 f ∧ Req2 𝔸 f }
+  { f : PermSet.FinsuppFunction 𝔸 𝔸 X | Req2 𝔸 f }
 
 def StepModel (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] : Type :=
   permissibleFunctions 𝔸 X
@@ -289,17 +292,6 @@ namespace StepModel
 
 variable {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X]
 
-private lemma permissibleFunctions_req1
-    (f : PermSet.FinsuppFunction 𝔸 𝔸 X) (π : FPerm 𝔸) : Req1 𝔸 f → Req1 𝔸 (π • f) := by
-  intro hf a
-  specialize hf (π⁻¹ • a)
-  rw [show NominalSet.supp 𝔸 (π • f) = π • NominalSet.supp 𝔸 f from Function.equivariant _ _ _ _]
-  rw [show ({a} : Set 𝔸) = π • {π⁻¹ • a} by simp]
-  rw [← Set.smul_set_union]
-  rw [PermSet.Finsupp.smul_val, PermSet.smul_function]
-  rw [← Rel.equivariant 𝔸 (PermSet.HasSupport 𝔸)]
-  exact hf
-
 private lemma permissibleFunctions_req2
     (f : PermSet.FinsuppFunction 𝔸 𝔸 X) (π : FPerm 𝔸) : Req2 𝔸 f → Req2 𝔸 (π • f) := by
   intro hf a c hcf hca
@@ -326,10 +318,7 @@ private lemma permissibleFunctions_req2
   simp
 
 instance : Set.Equivariant 𝔸 (permissibleFunctions 𝔸 X) := by
-  constructor; intro f π hf
-  constructor
-  · exact permissibleFunctions_req1 𝔸 f π hf.left
-  · exact permissibleFunctions_req2 𝔸 f π hf.right
+  constructor; exact permissibleFunctions_req2 𝔸
 
 instance : NominalSet 𝔸 (StepModel 𝔸 X) := Subtype.instNominalSetElem 𝔸
 
@@ -345,6 +334,13 @@ instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : StepModel
 @[simp] lemma fresh {a : 𝔸} {f : StepModel 𝔸 X} : a # f ↔ a # f.val :=
   Subtype.fresh 𝔸
 
+lemma choose_restriction (f : StepModel 𝔸 X) :
+    ∀ (a b c d : 𝔸), c # f → d # f → c ≠ a → d ≠ a → c ≠ b → d ≠ b →
+      (c \ (⸨a, c⸩ • f.val).val b) = (d \ (⸨a, d⸩ • f.val).val b) := by
+  intro a b c d hcf hdf hca hda hcb hdb
+  rw [fresh] at hcf hdf
+  exact choose_restriction' 𝔸 f.val a b c d hcf hdf hca hda hcb hdb
+
 private def bot' : PermSet.FinsuppFunction 𝔸 𝔸 X :=
   ⟨fun _ ↦ ⊥[𝔸], by
     use ∅; constructor
@@ -352,10 +348,6 @@ private def bot' : PermSet.FinsuppFunction 𝔸 𝔸 X :=
       simp [AlgebraStructure.bot_equivariant]
     · exact Set.finite_empty⟩
 
-private lemma bot_req1 : Req1 𝔸 (bot' 𝔸 : PermSet.FinsuppFunction 𝔸 𝔸 X) := by
-  intro a π _
-  apply AlgebraStructure.bot_equivariant
-
 private lemma bot_req2 : Req2 𝔸 (bot' 𝔸 : PermSet.FinsuppFunction 𝔸 𝔸 X) := by
   intro a c _ _
   simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, bot']
@@ -364,7 +356,7 @@ private lemma bot_req2 : Req2 𝔸 (bot' 𝔸 : PermSet.FinsuppFunction 𝔸 �
   rw [AlgebraStructure.ax_idempotent]
 
 def bot : Unit → StepModel 𝔸 X :=
-  fun _ ↦ ⟨bot' 𝔸, ⟨bot_req1 𝔸, bot_req2 𝔸⟩⟩
+  fun _ ↦ ⟨bot' 𝔸, bot_req2 𝔸⟩
 
 instance : Function.Equivariant 𝔸 (bot 𝔸 : Unit → StepModel 𝔸 X) := by
   constructor; intro _ π
@@ -387,24 +379,6 @@ private def union' : (StepModel 𝔸 X × StepModel 𝔸 X) → PermSet.FinsuppF
       apply NominalSet.supp_is_support
     · apply NominalSet.supp_finite⟩
 
-private lemma union_req1 {f g : StepModel 𝔸 X} : Req1 𝔸 (union' 𝔸 (f, g)) := by
-  intro a π hπ
-  have hπ₁ : π ∈ PermSet.fix 𝔸 (NominalSet.supp 𝔸 (union' 𝔸 (f, g))) := by
-    apply PermSet.fix_antitone_mem 𝔸 hπ; exact Set.subset_union_left
-  have hπ₂ : π • a = a := by
-    apply hπ; apply Set.mem_union_right; rfl
-  show π • (f.val.val a ∨[𝔸] g.val.val a) = (union' 𝔸 (f, g)).val a
-  rw [AlgebraStructure.join_equivariant]
-  rw [show π • f.val.val a = (π • f).val.val (π • a) by simp]
-  rw [show π • g.val.val a = (π • g).val.val (π • a) by simp]
-  rw [show ((π • f).val.val (π • a) ∨[𝔸] (π • g).val.val (π • a)) = (union' 𝔸 (π • f, π • g)).val (π • a) from rfl]
-  suffices union' 𝔸 (π • f, π • g) = π • union' 𝔸 (f, g) by
-    rw [this]
-    rw [show π • union' 𝔸 (f, g) = union' 𝔸 (f, g) from NominalSet.supp_is_support 𝔸 hπ₁]
-    rw [hπ₂]
-  ext b
-  simp [union', union'', AlgebraStructure.join_equivariant]
-
 private lemma union_req2 {f g : StepModel 𝔸 X} : Req2 𝔸 (union' 𝔸 (f, g)) := by
   intro a c hcfresh hca
   have hinf : (NominalSet.supp 𝔸 (union' 𝔸 (f, g)) ∪ NominalSet.supp 𝔸 f ∪ NominalSet.supp 𝔸 g ∪ {a})ᶜ.Infinite := by
@@ -424,7 +398,7 @@ private lemma union_req2 {f g : StepModel 𝔸 X} : Req2 𝔸 (union' 𝔸 (f, g
   have hdg : d # g.val := hd.left.right
   have hda : d ≠ a := hd.right
   simp only [PermSet.Finsupp.smul_val]
-  have h := Req1.choose_restriction 𝔸 (union' 𝔸 (f, g)) (union_req1 𝔸) a a c d hcfresh hdfresh hca hda hca hda
+  have h := choose_restriction' 𝔸 (union' 𝔸 (f, g)) a a c d hcfresh hdfresh hca hda hca hda
   simp only [PermSet.Finsupp.smul_val] at h
   rw [h]
   simp only [union', union'', PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap,
@@ -441,14 +415,14 @@ private lemma union_req2 {f g : StepModel 𝔸 X} : Req2 𝔸 (union' 𝔸 (f, g
   rw [← AlgebraStructure.ax_associative]
   nth_rw 4 [AlgebraStructure.ax_commutative]
   rw [show ⸨a, d⸩ • a = d by simp]
-  have hf := f.prop.right a d hdf hda
-  have hg := g.prop.right a d hdg hda
+  have hf := f.prop a d hdf hda
+  have hg := g.prop a d hdg hda
   simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap,
     Equiv.swap_apply_left] at hf hg
   rw [← hf, ← hg]
 
 def union : (StepModel 𝔸 X × StepModel 𝔸 X) → StepModel 𝔸 X :=
-  fun (f, g) ↦ ⟨union' 𝔸 (f, g), ⟨union_req1 𝔸, union_req2 𝔸⟩⟩
+  fun (f, g) ↦ ⟨union' 𝔸 (f, g), union_req2 𝔸⟩
 
 instance : Function.Equivariant 𝔸 (union 𝔸 : (StepModel 𝔸 X × StepModel 𝔸 X) → StepModel 𝔸 X) := by
   constructor; intro x π
@@ -457,17 +431,17 @@ instance : Function.Equivariant 𝔸 (union 𝔸 : (StepModel 𝔸 X × StepMode
   rw [show (π • x.fst, π • x.snd) = π • x by ext <;> simp]
   rw [← Function.equivariant]
 
-private noncomputable def chooseFresh (f : StepModel 𝔸 X) (a b : 𝔸) : 𝔸 :=
-  have hinf : (NominalSet.supp 𝔸 f ∪ {a} ∪ {b})ᶜ.Infinite := by
+private noncomputable def chooseFresh {X : Type} [NominalSet 𝔸 X] (x : X) (a b : 𝔸) : 𝔸 :=
+  have hinf : (NominalSet.supp 𝔸 x ∪ {a} ∪ {b})ᶜ.Infinite := by
     apply Set.Finite.infinite_compl
-    simp only [supp, Set.union_singleton, Set.finite_insert]
+    simp only [Set.union_singleton, Set.finite_insert]
     apply NominalSet.supp_finite
   Classical.choose hinf.nonempty
 
-private lemma chooseFresh_fresh (f : StepModel 𝔸 X) (a b : 𝔸) :
-    chooseFresh 𝔸 f a b # f.val ∧ chooseFresh 𝔸 f a b ≠ a ∧ chooseFresh 𝔸 f a b ≠ b := by
-  have h : chooseFresh 𝔸 f a b ∈ (NominalSet.supp 𝔸 f ∪ {a} ∪ {b})ᶜ := Classical.choose_spec _
-  simp only [supp, Set.union_singleton, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at h
+private lemma chooseFresh_fresh {X : Type} [NominalSet 𝔸 X] (x : X) (a b : 𝔸) :
+    chooseFresh 𝔸 x a b # x ∧ chooseFresh 𝔸 x a b ≠ a ∧ chooseFresh 𝔸 x a b ≠ b := by
+  have h : chooseFresh 𝔸 x a b ∈ (NominalSet.supp 𝔸 x ∪ {a} ∪ {b})ᶜ := Classical.choose_spec _
+  simp only [Set.union_singleton, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at h
   exact ⟨h.right.right, h.right.left, h.left⟩
 
 private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) → 𝔸 → X := Quotient.lift
@@ -482,7 +456,7 @@ private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) �
     | inl h => rw [h.left, h.right]
     | inr h =>
       simp only
-      have hinf : (NominalSet.supp 𝔸 f₁.val ∪ NominalSet.supp 𝔸 f₂.val ∪ {a₁} ∪ {a₂} ∪ {b})ᶜ.Infinite := by
+      have hinf : (NominalSet.supp 𝔸 f₁ ∪ NominalSet.supp 𝔸 f₂ ∪ {a₁} ∪ {a₂} ∪ {b})ᶜ.Infinite := by
         apply Set.Finite.infinite_compl
         rw [Set.finite_union, Set.finite_union, Set.finite_union, Set.finite_union]
         constructor
@@ -496,15 +470,15 @@ private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) �
         · apply Set.finite_singleton
       obtain ⟨c, hc⟩ := hinf.nonempty
       simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hc
-      have hcf₁ : c # f₁.val := hc.left.left.left.left
-      have hcf₂ : c # f₂.val := hc.left.left.left.right
+      have hcf₁ : c # f₁ := hc.left.left.left.left
+      have hcf₂ : c # f₂ := hc.left.left.left.right
       have hca₁ : c ≠ a₁ := hc.left.left.right
       have hca₂ : c ≠ a₂ := hc.left.right
       have hcb : c ≠ b := hc.right
       have ⟨hfreshf₁, hfresha₁, hfreshb₁⟩ := chooseFresh_fresh 𝔸 f₁ a₁ b
       have ⟨hfreshf₂, hfresha₂, hfreshb₂⟩ := chooseFresh_fresh 𝔸 f₂ a₂ b
-      rw [Req1.choose_restriction 𝔸 f₁.val f₁.prop.left a₁ b _ c hfreshf₁ hcf₁ hfresha₁ hca₁ hfreshb₁ hcb]
-      rw [Req1.choose_restriction 𝔸 f₂.val f₂.prop.left a₂ b _ c hfreshf₂ hcf₂ hfresha₂ hca₂ hfreshb₂ hcb]
+      rw [choose_restriction 𝔸 f₁ a₁ b _ c hfreshf₁ hcf₁ hfresha₁ hca₁ hfreshb₁ hcb]
+      rw [choose_restriction 𝔸 f₂ a₂ b _ c hfreshf₂ hcf₂ hfresha₂ hca₂ hfreshb₂ hcb]
       rw [h.right.right]
       suffices ⸨a₂,c⸩ • f₂.val = ⸨a₁,c⸩ • (⸨a₁,a₂⸩ • f₂).val by rw [this]
       rw [smul_val, ← MulAction.mul_smul]
@@ -520,7 +494,9 @@ private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) �
         contradiction
       · simp [*] at *
       · simp [*] at *
-      · simp [*] at *
+      · rw [← supp] at hd
+        rw [hdc] at hd
+        contradiction
       · simp only [Subgroup.coe_mul, Equiv.Perm.coe_mul, Function.comp_apply]
         rw [FPerm.swap_apply_of_ne_of_ne hda₂ hdc]
         rw [FPerm.swap_apply_of_ne_of_ne hda₁ hda₂]
@@ -535,9 +511,9 @@ instance : Function.Equivariant 𝔸 (restrict'' 𝔸 : NameAbstraction 𝔸 (St
   nth_rw 2 [PermSet.smul_function]
   have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 (π • f) (π • a) b
   have ⟨hdf, hda, hdb⟩ := chooseFresh_fresh 𝔸 f a (π⁻¹ • b)
-  have hcf' : π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b # f.val := by
+  have hcf' : π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b # f := by
     nth_rw 2 [show f = π⁻¹ • π • f by simp]
-    rw [← StepModel.fresh, ← Rel.equivariant 𝔸 NominalSet.IsFresh, StepModel.fresh]
+    rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
     exact hcf
   have hca' : π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b ≠ a := by
     intro hcontra
@@ -549,7 +525,7 @@ instance : Function.Equivariant 𝔸 (restrict'' 𝔸 : NameAbstraction 𝔸 (St
     have h : π • π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b = π • π⁻¹ • b := by rw [hcontra]
     rw [smul_inv_smul, smul_inv_smul] at h
     contradiction
-  have h := Req1.choose_restriction 𝔸 f.val f.prop.left a (π⁻¹ • b) _ _ hdf hcf' hda hca' hdb hcb'
+  have h := choose_restriction 𝔸 f a (π⁻¹ • b) _ _ hdf hcf' hda hca' hdb hcb'
   rw [PermSet.Finsupp.smul_val] at h
   rw [h, AlgebraStructure.res_equivariant, smul_inv_smul]
   rw [← MulAction.mul_smul]
@@ -568,48 +544,9 @@ private noncomputable def restrict' : NameAbstraction 𝔸 (StepModel 𝔸 X) �
       apply NominalSet.supp_is_support
     · apply NominalSet.supp_finite⟩
 
-private lemma restrict_req1 {a : 𝔸} {f : StepModel 𝔸 X} : Req1 𝔸 (restrict' 𝔸 (⟪a⟫ f)) := by
-  intro b π hπ
-  have hπ₁ : π ∈ PermSet.fix 𝔸 (NominalSet.supp 𝔸 (restrict' 𝔸 (⟪a⟫ f))) := by
-    apply PermSet.fix_antitone_mem 𝔸 hπ; exact Set.subset_union_left
-  have hπ₂ : π • b = b := by
-    apply hπ; apply Set.mem_union_right; rfl
-  show π • (chooseFresh 𝔸 f a b \ (⸨a,chooseFresh 𝔸 f a b⸩ • f.val).val b) = (restrict' 𝔸 (⟪a⟫ f)).val b
-  rw [AlgebraStructure.res_equivariant]
-  rw [PermSet.Finsupp.smul_val]
-  rw [show π • (⸨a,chooseFresh 𝔸 f a b⸩ • f.val.val) b = (π • ⸨a,chooseFresh 𝔸 f a b⸩ • f.val.val) (π • b) by simp]
-  rw [← MulAction.mul_smul]
-  rw [FPerm.mul_swap_eq_swap_mul]
-  rw [show ⸨π a,π (chooseFresh 𝔸 f a b)⸩ = ⸨π • a,π • (chooseFresh 𝔸 f a b)⸩ from rfl]
-  rw [MulAction.mul_smul]
-  let d := chooseFresh 𝔸 (π • f) (π • a) (π • b)
-  have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b
-  have ⟨hdf, hda, hdb⟩ := chooseFresh_fresh 𝔸 (π • f) (π • a) (π • b)
-  have hcf' : π • chooseFresh 𝔸 f a b # (π • f).val := by
-    rw [← StepModel.fresh, ← Rel.equivariant 𝔸 NominalSet.IsFresh, StepModel.fresh]
-    exact hcf
-  have hca' : π • chooseFresh 𝔸 f a b ≠ π • a := by
-    intro hcontra
-    have h : π⁻¹ • π • chooseFresh 𝔸 f a b = π⁻¹ • π • a := by rw [hcontra]
-    rw [inv_smul_smul, inv_smul_smul] at h; contradiction
-  have hcb' : π • chooseFresh 𝔸 f a b ≠ π • b := by
-    intro hcontra
-    have h : π⁻¹ • π • chooseFresh 𝔸 f a b = π⁻¹ • π • b := by rw [hcontra]
-    rw [inv_smul_smul, inv_smul_smul] at h; contradiction
-  have h := Req1.choose_restriction 𝔸 (π • f).val (π • f).prop.left (π • a) (π • b) _ _ hcf' hdf hca' hda hcb' hdb
-  rw [smul_val, PermSet.Finsupp.smul_val, PermSet.Finsupp.smul_val] at h
-  rw [h]
-  rw [show (d \ (⸨π • a,d⸩ • π • f.val).val (π • b)) = (restrict' 𝔸 (π • ⟪a⟫ f)).val (π • b) from rfl]
-  rw [show restrict' 𝔸 (π • ⟪a⟫ f) = π • restrict' 𝔸 (⟪a⟫ f) by
-    apply Subtype.eq
-    simp only [restrict', PermSet.Finsupp.smul_val]
-    rw [Function.equivariant 𝔸 (restrict'' 𝔸)]]
-  rw [show π • restrict' 𝔸 (⟪a⟫ f) = restrict' 𝔸 (⟪a⟫ f) from NominalSet.supp_is_support 𝔸 hπ₁]
-  rw [hπ₂]
-
 private lemma restrict_req2 {a : 𝔸} {f : StepModel 𝔸 X} : Req2 𝔸 (restrict' 𝔸 (⟪a⟫ f)) := by
   intro b c hcfresh hcb
-  have hinf : (NominalSet.supp 𝔸 f.val ∪ {a} ∪ {b} ∪ {c})ᶜ.Infinite := by
+  have hinf : (NominalSet.supp 𝔸 f ∪ {a} ∪ {b} ∪ {c})ᶜ.Infinite := by
     apply Set.Finite.infinite_compl
     rw [Set.finite_union, Set.finite_union, Set.finite_union]
     constructor
@@ -621,7 +558,7 @@ private lemma restrict_req2 {a : 𝔸} {f : StepModel 𝔸 X} : Req2 𝔸 (restr
     · apply Set.finite_singleton
   obtain ⟨d, hd⟩ := hinf.nonempty
   simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hd
-  have hdf : d # f.val := hd.left.left.left
+  have hdf : d # f := hd.left.left.left
   have hda : d ≠ a := hd.left.left.right
   have hdb : d ≠ b := hd.left.right
   have hdc : d ≠ c := hd.right
@@ -641,16 +578,16 @@ private lemma restrict_req2 {a : 𝔸} {f : StepModel 𝔸 X} : Req2 𝔸 (restr
   have hefresh : e # restrict' 𝔸 (⟪a⟫ f) := he.left.left.right
   have heb : e ≠ b := he.left.right
   have hed : e ≠ d := he.right
-  rw [Req1.choose_restriction 𝔸 (restrict' 𝔸 (⟪a⟫ f)) (restrict_req1 𝔸) b b _ _ hcfresh hefresh hcb heb hcb heb]
+  rw [choose_restriction' 𝔸 (restrict' 𝔸 (⟪a⟫ f)) b b _ _ hcfresh hefresh hcb heb hcb heb]
   simp only [restrict', restrict'', Quotient.lift_mk]
   nth_rw 3 [PermSet.Finsupp.smul_val]
   rw [PermSet.smul_function]
   simp only [FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left]
   have ⟨hdf₁, hda₁, hdb₁⟩ := chooseFresh_fresh 𝔸 f a b
   have ⟨hdf₂, hda₂, hde₂⟩ := chooseFresh_fresh 𝔸 f a e
-  rw [Req1.choose_restriction 𝔸 f.val f.prop.left a b _ _ hdf₁ hdf hda₁ hda hdb₁ hdb]
-  rw [Req1.choose_restriction 𝔸 f.val f.prop.left a e _ _ hdf₂ hdf hda₂ hda hde₂ (Ne.symm hed)]
-  have h := (⸨a,d⸩ • f).prop.right b e hef heb
+  rw [choose_restriction 𝔸 f a b _ _ hdf₁ hdf hda₁ hda hdb₁ hdb]
+  rw [choose_restriction 𝔸 f a e _ _ hdf₂ hdf hda₂ hda hde₂ (Ne.symm hed)]
+  have h := (⸨a,d⸩ • f).prop b e hef heb
   simp only [smul_val, PermSet.Finsupp.smul_val] at h
   nth_rw 3 [PermSet.smul_function] at h
   simp only [FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left] at h
@@ -662,15 +599,10 @@ private lemma restrict_req2 {a : 𝔸} {f : StepModel 𝔸 X} : Req2 𝔸 (restr
   rw [AlgebraStructure.ax_swap]
 
 noncomputable def restrict : NameAbstraction 𝔸 (StepModel 𝔸 X) → StepModel 𝔸 X :=
-  fun p ↦ ⟨restrict' 𝔸 p,
-  ⟨by
-    suffices ∀ p, Req1 𝔸 (restrict' 𝔸 p) by apply this
-    apply Quotient.ind; intro ⟨a, x⟩
-    apply restrict_req1,
-   by
+  fun p ↦ ⟨restrict' 𝔸 p, by
     suffices ∀ p, Req2 𝔸 (restrict' 𝔸 p) by apply this
     apply Quotient.ind; intro ⟨a, x⟩
-    apply restrict_req2⟩⟩
+    apply restrict_req2⟩
 
 instance : Function.Equivariant 𝔸 (restrict 𝔸 : NameAbstraction 𝔸 (StepModel 𝔸 X) → StepModel 𝔸 X) := by
   constructor; intro x π
@@ -692,8 +624,7 @@ lemma restrict_eq {a : 𝔸} {f : StepModel 𝔸 X} {b : 𝔸} :
       (restrict 𝔸 (⟪a⟫ f)).val.val b =  (c \ (⸨a, c⸩ • f.val).val b) := by
   intro d hdf hda hdb
   have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b
-  rw [fresh] at hdf
-  apply Req1.choose_restriction 𝔸 f.val f.prop.left a b _ _ hcf hdf hca hda hcb hdb
+  apply choose_restriction 𝔸 f a b _ _ hcf hdf hca hda hcb hdb
 
 lemma restrict_supp (f : StepModel 𝔸 X) (a c : 𝔸) :
     c # f → c # (restrict 𝔸 (⟪a⟫ f)) := by
@@ -710,7 +641,7 @@ lemma mem_fresh (f : StepModel 𝔸 X) (a c : 𝔸) : c # f → c ≠ a → c #
   intro hf hb hcontra
   rw [fresh] at hf
   have h : NominalSet.supp 𝔸 (f.val.val a) ⊆ NominalSet.supp 𝔸 f.val ∪ {a} :=
-    NominalSet.support_subset_supp 𝔸 (f.prop.left a) (by
+    NominalSet.support_subset_supp 𝔸 (supp_image 𝔸 f.val a) (by
       simp only [Set.union_singleton, Set.finite_insert]
       apply NominalSet.supp_finite)
   specialize h hcontra
@@ -742,13 +673,13 @@ noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where
     show restrict 𝔸 (⟪a⟫ f) = f
     apply Subtype.eq; apply Subtype.eq; ext b
     have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b
-    rw [restrict_eq']
-    rw [fresh] at hfresh
-    rw [show ⸨a,chooseFresh 𝔸 f a b⸩ • f.val = f.val from NominalSet.fresh_swap_fix 𝔸 hfresh hcf]
+    rw [restrict_eq', ← smul_val]
+    rw [show ⸨a,chooseFresh 𝔸 f a b⸩ • f = f from NominalSet.fresh_swap_fix 𝔸 hfresh hcf]
     apply AlgebraStructure.ax_fresh
     intro hcontra
-    have h := NominalSet.support_subset_supp 𝔸 (f.prop.left b) (by simp [NominalSet.supp_finite]) hcontra
+    have h := NominalSet.support_subset_supp 𝔸 (supp_image 𝔸 f.val b) (by simp [NominalSet.supp_finite]) hcontra
     simp only [Set.union_singleton, Set.mem_insert_iff] at h
+    rw [← supp] at h
     cases h <;> contradiction
   ax_swap a₁ a₂ f := by
     show restrict 𝔸 (⟪a₁⟫ (restrict 𝔸 (⟪a₂⟫ f))) = restrict 𝔸 (⟪a₂⟫ (restrict 𝔸 (⟪a₁⟫ f)))
@@ -854,11 +785,11 @@ noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where
     by_cases heq : a = b
     · rw [heq, restrict_eq']
       have ⟨hcf, hcb, _⟩ := chooseFresh_fresh 𝔸 f b b
-      exact f.prop.right b _ hcf hcb
+      rw [fresh] at hcf
+      exact f.prop b _ hcf hcb
     · rw [restrict_eq']
       let c := chooseFresh 𝔸 f a b
       have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b
-      rw [← fresh] at hcf
       rw [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv]
       rw [show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm heq) (Ne.symm hcb)]
       rw [show ⟪c⟫ ⸨a,c⸩ • f.val.val b = ⸨a,c⸩ • ⟪a⟫ f.val.val b by simp]
@@ -869,4 +800,130 @@ noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where
           apply mem_fresh 𝔸 f b c hcf hcb]
       apply AlgebraStructure.ax_redundant
 
+private lemma abs_choice {x : X} {a b : 𝔸} :
+    ∀ (c d : 𝔸), c # x → d # x → c ≠ a → d ≠ a → c ≠ b → d ≠ b →
+      ⸨b,c⸩ • (b \ (⸨a,c⸩ • x)) = ⸨b,d⸩ • (b \ (⸨a,d⸩ • x)) := by
+  intro c d hcx hdx hca hda hcb hdb
+  by_cases heq : c = d
+  · rw [heq]
+  · rw [AlgebraStructure.res_equivariant, AlgebraStructure.res_equivariant]
+    simp only [PermSet.atom_swap, Equiv.swap_apply_left]
+    suffices ⟪c⟫ ⸨b,c⸩ • ⸨a,c⸩ • x = ⟪d⟫ ⸨b,d⸩ • ⸨a,d⸩ • x by rw [this]
+    rw [NameAbstraction.eq_iff_cases]; right
+    constructor
+    · exact heq
+    · constructor
+      · rw [← show ⸨b,d⸩ • c = c from FPerm.swap_apply_of_ne_of_ne hcb heq]
+        rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
+        rw [← show ⸨a,d⸩ • c = c from FPerm.swap_apply_of_ne_of_ne hca heq]
+        rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
+        exact hcx
+      . nth_rw 2 [← MulAction.mul_smul]
+        rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne (Ne.symm hcb) (Ne.symm hdb)]
+        rw [MulAction.mul_smul]
+        nth_rw 3 [← MulAction.mul_smul]
+        rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne (Ne.symm hca) (Ne.symm hda)]
+        rw [MulAction.mul_smul]
+        rw [show ⸨c,d⸩ • x = x from NominalSet.fresh_swap_fix 𝔸 hcx hdx]
+
+private noncomputable def abs'' : NameAbstraction 𝔸 X → 𝔸 → X := Quotient.lift
+  (fun ⟨a, x⟩ b ↦
+    let c := chooseFresh 𝔸 x a b
+    ⸨b,c⸩ • (b \ (⸨a,c⸩ • x)))
+  (by
+    intro ⟨a, x⟩ ⟨a', x'⟩ haeq
+    ext b
+    simp only
+    rw [← NameAbstraction.eq_iff_alpha_eq 𝔸 X, NameAbstraction.eq_iff_cases] at haeq
+    cases haeq with
+    | inl h => rw [h.left, h.right]
+    | inr h =>
+      have hinf : (NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 x' ∪ {a} ∪ {a'} ∪ {b})ᶜ.Infinite := by
+        apply Set.Finite.infinite_compl
+        rw [Set.finite_union, Set.finite_union, Set.finite_union, Set.finite_union]
+        constructor
+        · constructor
+          · constructor
+            · constructor
+              · apply NominalSet.supp_finite
+              · apply NominalSet.supp_finite
+            · apply Set.finite_singleton
+          · apply Set.finite_singleton
+        · apply Set.finite_singleton
+      obtain ⟨c, hc⟩ := hinf.nonempty
+      simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hc
+      have hcx : c # x := hc.left.left.left.left
+      have hcx' : c # x' := hc.left.left.left.right
+      have hca : c ≠ a := hc.left.left.right
+      have hca' : c ≠ a' := hc.left.right
+      have hcb : c ≠ b := hc.right
+      have ⟨hdx, hda, hdb⟩ := chooseFresh_fresh 𝔸 x a b
+      rw [abs_choice 𝔸 _ _ hdx hcx hda hca hdb hcb]
+      have ⟨hex', hea', heb⟩ := chooseFresh_fresh 𝔸 x' a' b
+      rw [abs_choice 𝔸 _ _ hex' hcx' hea' hca' heb hcb]
+      suffices ⸨a,c⸩ • x = ⸨a',c⸩ • x' by rw [this]
+      rw [h.right.right, ← MulAction.mul_smul]
+      rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_left, FPerm.swap_apply_of_ne_of_ne (Ne.symm h.left) (Ne.symm hca')]
+      rw [MulAction.mul_smul, FPerm.swap_comm]
+      nth_rw 2 [NominalSet.fresh_swap_fix 𝔸]
+      · exact h.right.left
+      · exact hcx')
+
+instance : Function.Equivariant 𝔸 (abs'' 𝔸 : NameAbstraction 𝔸 X → 𝔸 → X) := by
+  constructor
+  apply Quotient.ind
+  intro ⟨a, x⟩ π
+  ext b
+  simp only [abs'', NameAbstraction.smul, Quotient.lift_mk, PermSet.smul_function]
+  have ⟨hcx, hca, hcb⟩ := chooseFresh_fresh 𝔸 (π • x) (π • a) b
+  have ⟨hdx, hda, hdb⟩ := chooseFresh_fresh 𝔸 x a (π⁻¹ • b)
+  have hcx' : π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b # x := by
+    nth_rw 2 [show x = π⁻¹ • π • x by simp]
+    rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
+    exact hcx
+  have hca' : π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b ≠ a := by
+    intro hcontra
+    have h : π • π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b = π • a := by rw [hcontra]
+    rw [smul_inv_smul] at h
+    contradiction
+  have hcb' : π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b ≠ π⁻¹ • b := by
+    intro hcontra
+    have h : π • π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b = π • π⁻¹ • b := by rw [hcontra]
+    rw [smul_inv_smul, smul_inv_smul] at h
+    contradiction
+  rw [abs_choice 𝔸 _ _ hdx hcx' hda hca' hdb hcb']
+  nth_rw 2 [← MulAction.mul_smul]
+  rw [show π * ⸨π⁻¹ • b,π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b⸩ = ⸨π • π⁻¹ • b,π • π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b⸩ * π from FPerm.mul_swap_eq_swap_mul]
+  rw [smul_inv_smul, smul_inv_smul, MulAction.mul_smul]
+  nth_rw 2 [AlgebraStructure.res_equivariant]
+  rw [smul_inv_smul]
+  nth_rw 2 [← MulAction.mul_smul]
+  rw [show π * ⸨a,π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b⸩ = ⸨π • a,π • π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b⸩ * π from FPerm.mul_swap_eq_swap_mul]
+  rw [smul_inv_smul, MulAction.mul_smul]
+
+private noncomputable def abs' : NameAbstraction 𝔸 X → PermSet.FinsuppFunction 𝔸 𝔸 X :=
+  fun p ↦ ⟨abs'' 𝔸 p, by
+    use NominalSet.supp 𝔸 p; constructor
+    · apply Function.Equivariant.preserve_support
+      apply NominalSet.supp_is_support
+    · apply NominalSet.supp_finite⟩
+
+
 end StepModel
+
+private noncomputable def ModelBundle (X : Type) [NominalSet 𝔸 X] : ℕ → ((T : Type) × ((_ : NominalSet 𝔸 T) × AlgebraStructure 𝔸 T))
+| 0 => ⟨BaseModel 𝔸 X, inferInstance, inferInstance⟩
+| n + 1 =>
+  let ⟨Y, _, _⟩ := ModelBundle X n
+  ⟨StepModel 𝔸 Y, inferInstance, inferInstance⟩
+
+def Model (X : Type) [NominalSet 𝔸 X] (n : ℕ) := (ModelBundle 𝔸 X n).fst
+
+namespace Model
+
+variable {X : Type} [NominalSet 𝔸 X] {n : ℕ}
+
+noncomputable instance : NominalSet 𝔸 (Model 𝔸 X n) := (ModelBundle 𝔸 X n).snd.fst
+noncomputable instance : AlgebraStructure 𝔸 (Model 𝔸 X n) := (ModelBundle 𝔸 X n).snd.snd
+
+end Model