1 files changed, 247 insertions, 60 deletions
diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean
index 7cc0df6..9c6103f 100644
--- a/Nominal/NameRestriction/Model.lean
+++ b/Nominal/NameRestriction/Model.lean
@@ -214,46 +214,66 @@ def Req1 {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.F
 
 lemma Req1.choose_restriction
     {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :
-    Req1 𝔸 f → ∀ (a c d : 𝔸), c # f → d # f → c ≠ a → d ≠ a →
-      (c \ (⸨a, c⸩ • f).val a) = (d \ (⸨a, d⸩ • f).val a) := by
-  intro hreq a c d hcfresh hdfresh hca hda
-  nth_rw 1 [← show ⸨c, d⸩ • f = f from NominalSet.fresh_swap_fix 𝔸 hcfresh hdfresh]
-  simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap,
-    Equiv.swap_apply_left]
-  rw [show ⟪d⟫ ⸨a,d⸩ • f.val d = ⟪⸨a, d⸩ • a⟫ ⸨a,d⸩ • f.val d by simp]
-  rw [show ⟪⸨a, d⸩ • a⟫ ⸨a,d⸩ • f.val d = ⸨a, d⸩ • ⟪a⟫ f.val d by simp]
-  rw [show ⟪c⟫ ⸨a,c⸩ • ⸨c, d⸩ • f.val d = ⟪⸨a, c⸩ • a⟫ ⸨a,c⸩ • ⸨c, d⸩ • f.val d by simp]
-  rw [show ⟪⸨a, c⸩ • a⟫ ⸨a,c⸩ • ⸨c, d⸩ • f.val d = ⸨a, c⸩ • ⟪a⟫ ⸨c, d⸩ • f.val d by simp]
-  nth_rw 2 [show a = ⸨c, d⸩ • a by
-    symm; apply FPerm.swap_apply_of_ne_of_ne
-    · symm; exact hca
-    · symm; exact hda]
-  rw [show ⟪⸨c, d⸩ • a⟫ ⸨c,d⸩ • f.val d = ⸨c, d⸩ • ⟪a⟫ f.val d by simp]
-  suffices ⸨a,c⸩ • ⸨c,d⸩ • ⟪a⟫ f.val d = ⸨a,d⸩ • ⟪a⟫ f.val d by rw [this]
-  rw [← MulAction.mul_smul]
-  apply PermSet.support_permutations_eq 𝔸 (NominalSet.supp_is_support 𝔸)
-  intro b hb
-  by_cases hba : b = a <;> by_cases hbc : b = c <;> by_cases hbd : b = d
-  · simp [*] at *
-  · simp [*] at *
-  · simp [*] at *
-  · simp [*] at *
-  · rw [← hbc, ← hbd]; simp
-  · rw [hbc] at hb
-    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])
-    specialize h hc
-    simp only [Set.union_singleton, Set.mem_insert_iff] at h
-    cases h
+    Req1 𝔸 f → ∀ (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
+  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,
+      PermSet.atom_swap, Equiv.swap_apply_left]
+    rw [show ⟪d⟫ ⸨a,d⸩ • f.val d = ⸨a, d⸩ • ⟪a⟫ f.val d by simp]
+    rw [show ⟪c⟫ ⸨a,c⸩ • ⸨c, d⸩ • f.val d = ⸨a, c⸩ • ⟪a⟫ ⸨c, d⸩ • f.val d by simp]
+    nth_rw 2 [show a = ⸨c, d⸩ • a by
+      symm; apply FPerm.swap_apply_of_ne_of_ne
+      · symm; exact hca
+      · symm; exact hda]
+    rw [show ⟪⸨c, d⸩ • a⟫ ⸨c,d⸩ • f.val d = ⸨c, d⸩ • ⟪a⟫ f.val d by simp]
+    suffices ⸨a,c⸩ • ⸨c,d⸩ • ⟪a⟫ f.val d = ⸨a,d⸩ • ⟪a⟫ f.val d by rw [this]
+    rw [← MulAction.mul_smul]
+    apply PermSet.support_permutations_eq 𝔸 (NominalSet.supp_is_support 𝔸)
+    intro b hb
+    by_cases hba : b = a <;> by_cases hbc : b = c <;> by_cases hbd : b = d
+    · simp [*] at *
+    · simp [*] at *
+    · simp [*] at *
+    · simp [*] at *
+    · rw [← hbc, ← hbd]; simp
+    · rw [hbc] at hb
+      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])
+      specialize h hc
+      simp only [Set.union_singleton, Set.mem_insert_iff] at h
+      cases h
+      · simp [*] at *
+      · contradiction
     · simp [*] at *
-    · contradiction
-  · simp [*] at *
-  · simp only [Subgroup.coe_mul, Equiv.Perm.coe_mul, Function.comp_apply]
-    rw [FPerm.swap_apply_of_ne_of_ne hbc hbd]
-    rw [FPerm.swap_apply_of_ne_of_ne hba hbc]
-    rw [FPerm.swap_apply_of_ne_of_ne hba hbd]
+    · simp only [Subgroup.coe_mul, Equiv.Perm.coe_mul, Function.comp_apply]
+      rw [FPerm.swap_apply_of_ne_of_ne hbc hbd]
+      rw [FPerm.swap_apply_of_ne_of_ne hba hbc]
+      rw [FPerm.swap_apply_of_ne_of_ne hba hbd]
+  · simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap]
+    rw [Equiv.swap_apply_of_ne_of_ne heq (Ne.symm hcb)]
+    rw [Equiv.swap_apply_of_ne_of_ne heq (Ne.symm hdb)]
+    rw [show ⟪c⟫ ⸨a,c⸩ • f.val b = ⸨a,c⸩ • ⟪a⟫ f.val b by simp]
+    rw [show ⟪d⟫ ⸨a,d⸩ • f.val b = ⸨a,d⸩ • ⟪a⟫ f.val b by simp]
+    rw [show ⸨a,c⸩ • ⟪a⟫ f.val b = ⟪a⟫ f.val b by
+      apply NominalSet.fresh_swap_fix
+      · 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
+        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
+      apply NominalSet.fresh_swap_fix
+      · 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
+        simp only [Set.union_singleton, Set.mem_insert_iff] at h
+        cases h <;> contradiction]
 
 def Req2 {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :=
   -- Traces for all atoms include those from bound traces
@@ -404,7 +424,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 c d hcfresh hdfresh hca hda
+  have h := Req1.choose_restriction 𝔸 (union' 𝔸 (f, g)) (union_req1 𝔸) 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,
@@ -437,23 +457,23 @@ 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 : 𝔸) : 𝔸 :=
-  have hinf : (NominalSet.supp 𝔸 f ∪ {a})ᶜ.Infinite := by
+private noncomputable def chooseFresh (f : StepModel 𝔸 X) (a b : 𝔸) : 𝔸 :=
+  have hinf : (NominalSet.supp 𝔸 f ∪ {a} ∪ {b})ᶜ.Infinite := by
     apply Set.Finite.infinite_compl
     simp only [supp, Set.union_singleton, Set.finite_insert]
     apply NominalSet.supp_finite
   Classical.choose hinf.nonempty
 
-private lemma chooseFresh_fresh (f : StepModel 𝔸 X) (a : 𝔸) :
-    chooseFresh 𝔸 f a # f.val ∧ chooseFresh 𝔸 f a ≠ a := by
-  have h : chooseFresh 𝔸 f a ∈ (NominalSet.supp 𝔸 f ∪ {a})ᶜ := Classical.choose_spec _
+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
-  exact ⟨h.right, h.left⟩
+  exact ⟨h.right.right, h.right.left, h.left⟩
 
 private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) → 𝔸 → X := Quotient.lift
-  (fun ⟨a, f⟩ ↦
-    let c := chooseFresh 𝔸 f a
-    fun b ↦ if a = b then (c \ (⸨a, c⸩ • f.val).val a) else f.val.val b)
+  (fun ⟨a, f⟩ b ↦
+    let c := chooseFresh 𝔸 f a b
+    (c \ (⸨a, c⸩ • f.val).val b))
   (by
     intro ⟨a₁, f₁⟩ ⟨a₂, f₂⟩ haeq
     ext b
@@ -461,17 +481,184 @@ private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) �
     cases haeq with
     | inl h => rw [h.left, h.right]
     | inr h =>
-      simp only [PermSet.Finsupp.smul_val]
-      by_cases h₁ : a₁ = b <;> by_cases h₂ : a₂ = b <;> simp only [h₁, h₂, ↓reduceIte]
-      · rw [← h₂] at h₁
-        have hcontra := h.left
+      simp only
+      have hinf : (NominalSet.supp 𝔸 f₁.val ∪ NominalSet.supp 𝔸 f₂.val ∪ {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 hcf₁ : c # f₁.val := hc.left.left.left.left
+      have hcf₂ : c # f₂.val := 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 [h.right.right]
+      suffices ⸨a₂,c⸩ • f₂.val = ⸨a₁,c⸩ • (⸨a₁,a₂⸩ • f₂).val by rw [this]
+      rw [smul_val, ← MulAction.mul_smul]
+      apply PermSet.support_permutations_eq 𝔸 (NominalSet.supp_is_support 𝔸)
+      intro d hd
+      by_cases hda₁ : d = a₁ <;> by_cases hda₂ : d = a₂ <;> by_cases hdc : d = c
+      · simp [*] at *
+      · simp [*] at *
+      · simp [*] at *
+      · rw [hda₁] at hd
+        have hcontra : a₁ ∉ NominalSet.supp 𝔸 f₂ := h.right.left
+        rw [StepModel.supp] at hcontra
         contradiction
-      ·
-        sorry
-      · rw [h.right.right, ← h₂]
-        simp only [smul_val, PermSet.Finsupp.smul_val]
-        have heq := Req1.choose_restriction 𝔸 f₂.val f₂.prop.left
-        sorry
-      · sorry)
+      · simp [*] at *
+      · simp [*] at *
+      · simp [*] at *
+      · 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₂]
+        rw [FPerm.swap_apply_of_ne_of_ne hda₁ hdc])
+
+instance : Function.Equivariant 𝔸 (restrict'' 𝔸 : NameAbstraction 𝔸 (StepModel 𝔸 X) → 𝔸 → X) := by
+  constructor
+  apply Quotient.ind
+  intro ⟨a, f⟩ π
+  ext b
+  simp only [restrict'', PermSet.Finsupp.smul_val, NameAbstraction.smul, Quotient.lift_mk, smul_val]
+  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
+    nth_rw 2 [show f = π⁻¹ • π • f by simp]
+    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 [smul_inv_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 [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'
+  rw [PermSet.Finsupp.smul_val] at h
+  rw [h, AlgebraStructure.res_equivariant, smul_inv_smul]
+  rw [← MulAction.mul_smul]
+  rw [show ⸨π • a,chooseFresh 𝔸 (π • f) (π • a) b⸩ * π = π * ⸨a, π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b⸩ by
+    rw [FPerm.mul_swap_eq_swap_mul]
+    rw [show π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b = π⁻¹ (chooseFresh 𝔸 (π • f) (π • a) b) from rfl]
+    rw [show π • a = π a from rfl]
+    simp]
+  rw [MulAction.mul_smul]
+  simp
+
+private noncomputable def restrict' : NameAbstraction 𝔸 (StepModel 𝔸 X) → PermSet.FinsuppFunction 𝔸 𝔸 X :=
+  fun p ↦ ⟨restrict'' 𝔸 p, by
+    use NominalSet.supp 𝔸 p; constructor
+    · apply Function.Equivariant.preserve_support
+      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
+    apply Set.Finite.infinite_compl
+    rw [Set.finite_union, Set.finite_union, Set.finite_union]
+    constructor
+    · constructor
+      · constructor
+        · apply NominalSet.supp_finite
+        · apply Set.finite_singleton
+      · apply Set.finite_singleton
+    · 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 hda : d ≠ a := hd.left.left.right
+  have hdb : d ≠ b := hd.left.right
+  have hdc : d ≠ c := hd.right
+  have hinf' : (NominalSet.supp 𝔸 (⸨a, d⸩ • f).val ∪ NominalSet.supp 𝔸 (restrict' 𝔸 (⟪a⟫ f)) ∪ {b} ∪ {d})ᶜ.Infinite := by
+    apply Set.Finite.infinite_compl
+    rw [Set.finite_union, Set.finite_union, Set.finite_union]
+    constructor
+    · constructor
+      · constructor
+        · apply NominalSet.supp_finite
+        · apply NominalSet.supp_finite
+      · apply Set.finite_singleton
+    · apply Set.finite_singleton
+  obtain ⟨e, he⟩ := hinf'.nonempty
+  simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at he
+  have hef : e # (⸨a, d⸩ • f).val := he.left.left.left
+  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]
+  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
+  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
+  simp only [PermSet.Finsupp.smul_val]
+  nth_rw 1 [h]
+  rw [AlgebraStructure.ax_distributive]
+  rw [AlgebraStructure.res_equivariant]
+  rw [show ⸨b,e⸩ • d = d from FPerm.swap_apply_of_ne_of_ne hdb (Ne.symm hed)]
+  rw [AlgebraStructure.ax_swap]
 
 end StepModel