diff --git a/ConNF/Aux/Rel.lean b/ConNF/Aux/Rel.lean
index ec1f6f251a..0311064602 100644
--- a/ConNF/Aux/Rel.lean
+++ b/ConNF/Aux/Rel.lean
@@ -80,6 +80,10 @@ theorem codomEqDom_iff' (r : Rel α α) :
 theorem OneOne.inv {r : Rel α β} (h : r.OneOne) : r.inv.OneOne :=
   ⟨⟨h.coinjective⟩, ⟨h.injective⟩⟩
 
+theorem inv_apply {r : Rel α β} {x : α} {y : β} :
+    r.inv y x ↔ r x y :=
+  Iff.rfl
+
 theorem inv_injective : Function.Injective (inv : Rel α β → Rel β α) := by
   intro r s h
   ext a b : 2
diff --git a/ConNF/Counting/CodingFunction.lean b/ConNF/Counting/CodingFunction.lean
index 821a0feef5..b2358dc5d8 100644
--- a/ConNF/Counting/CodingFunction.lean
+++ b/ConNF/Counting/CodingFunction.lean
@@ -87,13 +87,13 @@ theorem ext_aux {χ₁ χ₂ : CodingFunction β} {S : Support β} {x : TSet β}
   exact χ₂.smul_rel h₂ ρ
 
 theorem ext {χ₁ χ₂ : CodingFunction β} (S : Support β) (x : TSet β)
-    (h : χ₁.rel S x ∧ χ₂.rel S x) :
+    (h₁ : χ₁.rel S x) (h₂ : χ₂.rel S x) :
     χ₁ = χ₂ := by
   apply ext'
   intro _ _
   constructor
-  · apply ext_aux h.1 h.2
-  · apply ext_aux h.2 h.1
+  · apply ext_aux h₁ h₂
+  · apply ext_aux h₂ h₁
 
 end CodingFunction
 
@@ -122,4 +122,19 @@ theorem Tangle.code_rel_self (t : Tangle β) :
   use 1
   simp only [allPermForget_one, one_smul, and_self]
 
+theorem Tangle.code_eq_code_iff (t₁ t₂ : Tangle β) :
+    t₁.code = t₂.code ↔ ∃ ρ : AllPerm β, ρ • t₁ = t₂ := by
+  constructor
+  · intro h
+    have := t₂.code_rel_self
+    rw [← h] at this
+    obtain ⟨ρ, hρ₁, hρ₂⟩ := this
+    use ρ
+    exact Tangle.ext hρ₂ hρ₁
+  · rintro ⟨ρ, rfl⟩
+    symm
+    apply CodingFunction.ext _ _ (ρ • t₁).code_rel_self
+    use ρ
+    exact ⟨rfl, rfl⟩
+
 end ConNF
diff --git a/ConNF/Counting/Spec.lean b/ConNF/Counting/Spec.lean
index 3febb8baec..f9d9978aba 100644
--- a/ConNF/Counting/Spec.lean
+++ b/ConNF/Counting/Spec.lean
@@ -65,6 +65,30 @@ instance (β : TypeIndex) [LeLevel β] :
 
 variable {β : TypeIndex} [LeLevel β]
 
+@[ext]
+theorem Spec.ext {σ τ : Spec β} (h₁ : ∀ A, σᴬ A = τᴬ A) (h₂ : ∀ A, σᴺ A = τᴺ A) : σ = τ := by
+  obtain ⟨σa, σN⟩ := σ
+  obtain ⟨τa, τN⟩ := τ
+  rw [mk.injEq]
+  constructor
+  · funext A
+    exact h₁ A
+  · funext A
+    exact h₂ A
+
+instance : LE (Spec β) where
+  le σ τ := ∀ A,
+    (σᴬ A).bound = (τᴬ A).bound ∧ (σᴬ A).rel ≤ (τᴬ A).rel ∧
+    (σᴺ A).bound = (τᴺ A).bound ∧ (σᴺ A).rel ≤ (τᴺ A).rel
+
+instance : PartialOrder (Spec β) where
+  le_refl σ A := ⟨rfl, le_rfl, rfl, le_rfl⟩
+  le_trans σ τ υ h₁ h₂ A := ⟨(h₁ A).1.trans (h₂ A).1, (h₁ A).2.1.trans (h₂ A).2.1,
+    (h₁ A).2.2.1.trans (h₂ A).2.2.1, (h₁ A).2.2.2.trans (h₂ A).2.2.2⟩
+  le_antisymm σ τ h₁ h₂ := Spec.ext
+    (λ A ↦ Enumeration.ext (h₁ A).1 (le_antisymm (h₁ A).2.1 (h₂ A).2.1))
+    (λ A ↦ Enumeration.ext (h₁ A).2.2.1 (le_antisymm (h₁ A).2.2.2 (h₂ A).2.2.2))
+
 def nearLitterCondRelFlex (S : Support β) (A : β ↝ ⊥) :
     Rel NearLitter (NearLitterCond β) :=
   λ N c ↦ ¬Inflexible A Nᴸ ∧ c = .flex ⟨{i | ∃ N', (S ⇘. A)ᴺ.rel i N' ∧ Nᴸ = N'ᴸ}⟩
@@ -115,6 +139,19 @@ theorem nearLitterCondRel_dom_disjoint {S : Support β} {A : β ↝ ⊥} :
   exact flexible_of_mem_dom_nearLitterCondFlexRel hN₁
     (inflexible_of_mem_dom_nearLitterCondInflexRel hN₂)
 
+theorem nearLitterCondRel_inflex {S : Support β} {A : β ↝ ⊥} {N : NearLitter}
+    {P : InflexiblePath β} {χ : CodingFunction P.δ} {ta tn : Tree (Rel κ κ) P.δ} :
+    nearLitterCondRel S A N (.inflex P ⟨χ, ta, tn⟩) →
+    ∃ t : Tangle P.δ, A = P.A ↘ P.hε ↘. ∧ Nᴸ = fuzz P.hδε t ∧ χ = t.code ∧
+      (ta = λ B ↦ (S ⇘. (P.A ↘ P.hδ ⇘ B))ᴬ.rel.comp (t.support ⇘. B)ᴬ.rel.inv) ∧
+      (tn = λ B ↦ (S ⇘. (P.A ↘ P.hδ ⇘ B))ᴺ.rel.comp (t.support ⇘. B)ᴺ.rel.inv) := by
+  rintro (⟨_, h⟩ | ⟨P', t, hA, ht, h⟩)
+  · cases h
+  · rw [NearLitterCond.inflex.injEq] at h
+    cases h.1
+    rw [heq_eq_eq, InflexCond.mk.injEq] at h
+    exact ⟨t, hA, ht, h.2⟩
+
 theorem nearLitterCondRel_coinjective (S : Support β) (A : β ↝ ⊥) :
     (nearLitterCondRel S A).Coinjective :=
   Rel.sup_coinjective
@@ -136,6 +173,16 @@ def Support.spec (S : Support β) : Spec β where
   nearLitters A := (S ⇘. A)ᴺ.comp
     (nearLitterCondRel S A) (nearLitterCondRel_coinjective S A)
 
+theorem Support.spec_atoms (S : Support β) (A : β ↝ ⊥) :
+    S.specᴬ A = (S ⇘. A)ᴬ.image
+      (λ a ↦ ⟨{i | (S ⇘. A)ᴬ.rel i a}, {i | ∃ N, (S ⇘. A)ᴺ.rel i N ∧ a ∈ Nᴬ}⟩) :=
+  rfl
+
+theorem Support.spec_nearLitters (S : Support β) (A : β ↝ ⊥) :
+    S.specᴺ A = (S ⇘. A)ᴺ.comp
+      (nearLitterCondRel S A) (nearLitterCondRel_coinjective S A) :=
+  rfl
+
 theorem Support.spec_atoms_dom (S : Support β) (A : β ↝ ⊥) :
     (S.specᴬ A).rel.dom = (S ⇘. A)ᴬ.rel.dom := by
   ext i
@@ -180,6 +227,8 @@ def atomMemRel (S : Support β) (A : β ↝ ⊥) : Rel κ κ :=
   (S ⇘. A)ᴺ.rel.comp (Rel.comp (λ N a ↦ a ∈ Nᴬ) (S ⇘. A)ᴬ.rel.inv)
 
 structure SameSpec (S T : Support β) : Prop where
+(atoms_bound_eq : ∀ A, (S ⇘. A)ᴬ.bound = (T ⇘. A)ᴬ.bound)
+(nearLitters_bound_eq : ∀ A, (S ⇘. A)ᴺ.bound = (T ⇘. A)ᴺ.bound)
 (atoms_dom_eq : ∀ A, (S ⇘. A)ᴬ.rel.dom = (T ⇘. A)ᴬ.rel.dom)
 (nearLitters_dom_eq : ∀ A, (S ⇘. A)ᴺ.rel.dom = (T ⇘. A)ᴺ.rel.dom)
 (convAtoms_oneOne : ∀ A, (convAtoms S T A).OneOne)
@@ -190,17 +239,18 @@ structure SameSpec (S T : Support β) : Prop where
   (∃ ρ : AllPerm P.δ, N₂ᴸ = fuzz P.hδε (ρ • t))))
 (litter_eq_iff_of_flexible : ∀ {A N₁ N₂ N₃ N₄},
   convNearLitters S T A N₁ N₂ → convNearLitters S T A N₃ N₄ →
-  ¬Inflexible A N₁ᴸ → ¬Inflexible A N₂ᴸ → (N₁ᴸ = N₃ᴸ ↔ N₂ᴸ = N₄ᴸ))
+  ¬Inflexible A N₁ᴸ → ¬Inflexible A N₂ᴸ → ¬Inflexible A N₃ᴸ → ¬Inflexible A N₄ᴸ →
+  (N₁ᴸ = N₃ᴸ ↔ N₂ᴸ = N₄ᴸ))
 (convAtoms_of_inflexible : ∀ A, ∀ N₁ N₂ : NearLitter,
   ∀ P : InflexiblePath β, ∀ t : Tangle P.δ, ∀ ρ : AllPerm P.δ,
-  A = P.A ↘ P.hε ↘. ∧ N₁ᴸ = fuzz P.hδε t → N₂ᴸ = fuzz P.hδε (ρ • t) →
-  ∀ B : P.δ ↝ ⊥,
+  A = P.A ↘ P.hε ↘. → N₁ᴸ = fuzz P.hδε t → N₂ᴸ = fuzz P.hδε (ρ • t) →
+  convNearLitters S T A N₁ N₂ → ∀ B : P.δ ↝ ⊥,
     convAtoms (S ⇘ (P.A ↘ P.hδ)) (T ⇘ (P.A ↘ P.hδ)) B ⊓ (λ a _ ↦ a ∈ (t.support ⇘. B)ᴬ) ≤
       (λ a b ↦ b = ρᵁ ⇘. B • a))
 (convNearLitters_of_inflexible : ∀ A, ∀ N₁ N₂ : NearLitter,
   ∀ P : InflexiblePath β, ∀ t : Tangle P.δ, ∀ ρ : AllPerm P.δ,
-  A = P.A ↘ P.hε ↘. ∧ N₁ᴸ = fuzz P.hδε t → N₂ᴸ = fuzz P.hδε (ρ • t) →
-  ∀ B : P.δ ↝ ⊥,
+  A = P.A ↘ P.hε ↘. → N₁ᴸ = fuzz P.hδε t → N₂ᴸ = fuzz P.hδε (ρ • t) →
+  convNearLitters S T A N₁ N₂ → ∀ B : P.δ ↝ ⊥,
     convNearLitters (S ⇘ (P.A ↘ P.hδ)) (T ⇘ (P.A ↘ P.hδ)) B ⊓ (λ a _ ↦ a ∈ (t.support ⇘. B)ᴺ) ≤
       (λ N₁ N₂ ↦ N₂ = ρᵁ ⇘. B • N₁))
 
@@ -208,6 +258,8 @@ structure SameSpec (S T : Support β) : Prop where
 implications. It can sometimes be easier to prove this in generality than to prove `SameSpec`
 directly. -/
 structure SameSpecLE (S T : Support β) : Prop where
+(atoms_bound_eq : ∀ A, (S ⇘. A)ᴬ.bound = (T ⇘. A)ᴬ.bound)
+(nearLitters_bound_eq : ∀ A, (S ⇘. A)ᴺ.bound = (T ⇘. A)ᴺ.bound)
 (atoms_dom_subset : ∀ A, (S ⇘. A)ᴬ.rel.dom ⊆ (T ⇘. A)ᴬ.rel.dom)
 (nearLitters_dom_subset : ∀ A, (S ⇘. A)ᴺ.rel.dom ⊆ (T ⇘. A)ᴺ.rel.dom)
 (convAtoms_injective : ∀ A, (convAtoms S T A).Injective)
@@ -217,22 +269,25 @@ structure SameSpecLE (S T : Support β) : Prop where
   N₁ᴸ = fuzz P.hδε t → ∃ ρ : AllPerm P.δ, N₂ᴸ = fuzz P.hδε (ρ • t))
 (litter_eq_of_flexible : ∀ {A N₁ N₂ N₃ N₄},
   convNearLitters S T A N₁ N₂ → convNearLitters S T A N₃ N₄ →
-  ¬Inflexible A N₁ᴸ → ¬Inflexible A N₂ᴸ → (N₁ᴸ = N₃ᴸ → N₂ᴸ = N₄ᴸ))
+  ¬Inflexible A N₁ᴸ → ¬Inflexible A N₂ᴸ → ¬Inflexible A N₃ᴸ → ¬Inflexible A N₄ᴸ →
+  N₁ᴸ = N₃ᴸ → N₂ᴸ = N₄ᴸ)
 (convAtoms_of_inflexible : ∀ A, ∀ N₁ N₂ : NearLitter,
   ∀ P : InflexiblePath β, ∀ t : Tangle P.δ, ∀ ρ : AllPerm P.δ,
-  A = P.A ↘ P.hε ↘. ∧ N₁ᴸ = fuzz P.hδε t → N₂ᴸ = fuzz P.hδε (ρ • t) →
-  ∀ B : P.δ ↝ ⊥,
+  A = P.A ↘ P.hε ↘. → N₁ᴸ = fuzz P.hδε t → N₂ᴸ = fuzz P.hδε (ρ • t) →
+  convNearLitters S T A N₁ N₂ → ∀ B : P.δ ↝ ⊥,
     convAtoms (S ⇘ (P.A ↘ P.hδ)) (T ⇘ (P.A ↘ P.hδ)) B ⊓ (λ a _ ↦ a ∈ (t.support ⇘. B)ᴬ) ≤
       (λ a b ↦ b = ρᵁ ⇘. B • a))
 (convNearLitters_of_inflexible : ∀ A, ∀ N₁ N₂ : NearLitter,
   ∀ P : InflexiblePath β, ∀ t : Tangle P.δ, ∀ ρ : AllPerm P.δ,
-  A = P.A ↘ P.hε ↘. ∧ N₁ᴸ = fuzz P.hδε t → N₂ᴸ = fuzz P.hδε (ρ • t) →
-  ∀ B : P.δ ↝ ⊥,
+  A = P.A ↘ P.hε ↘. → N₁ᴸ = fuzz P.hδε t → N₂ᴸ = fuzz P.hδε (ρ • t) →
+  convNearLitters S T A N₁ N₂ → ∀ B : P.δ ↝ ⊥,
     convNearLitters (S ⇘ (P.A ↘ P.hδ)) (T ⇘ (P.A ↘ P.hδ)) B ⊓ (λ a _ ↦ a ∈ (t.support ⇘. B)ᴺ) ≤
       (λ N₁ N₂ ↦ N₂ = ρᵁ ⇘. B • N₁))
 
 theorem sameSpec_antisymm {S T : Support β} (h₁ : SameSpecLE S T) (h₂ : SameSpecLE T S) :
     SameSpec S T where
+  atoms_bound_eq := h₁.atoms_bound_eq
+  nearLitters_bound_eq := h₁.nearLitters_bound_eq
   atoms_dom_eq A := subset_antisymm (h₁.atoms_dom_subset A) (h₂.atoms_dom_subset A)
   nearLitters_dom_eq A := subset_antisymm (h₁.nearLitters_dom_subset A) (h₂.nearLitters_dom_subset A)
   convAtoms_oneOne A := ⟨h₁.convAtoms_injective A,
@@ -248,9 +303,11 @@ theorem sameSpec_antisymm {S T : Support β} (h₁ : SameSpecLE S T) (h₂ : Sam
       obtain ⟨ρ', ht'⟩ := h₂.inflexible_of_inflexible (convNearLitters_inv T S _ ▸ h) P (ρ • t) hA ht
       use ρ' * ρ
       rw [ht', mul_smul]
-  litter_eq_iff_of_flexible hN₁ hN₂ hN₁' hN₂' := ⟨h₁.litter_eq_of_flexible hN₁ hN₂ hN₁' hN₂',
-    h₂.litter_eq_of_flexible
-      (convNearLitters_inv S T _ ▸ hN₁) (convNearLitters_inv S T _ ▸ hN₂) hN₂' hN₁'⟩
+  litter_eq_iff_of_flexible hN₁ hN₂ hN₁' hN₂' hN₃' hN₄' := by
+    refine ⟨h₁.litter_eq_of_flexible hN₁ hN₂ hN₁' hN₂' hN₃' hN₄', ?_⟩
+    have := h₂.litter_eq_of_flexible
+      (convNearLitters_inv T S _ ▸ hN₁) (convNearLitters_inv T S _ ▸ hN₂)
+    apply this <;> assumption
   convAtoms_of_inflexible := h₁.convAtoms_of_inflexible
   convNearLitters_of_inflexible := h₁.convNearLitters_of_inflexible
 
@@ -258,6 +315,57 @@ namespace Support
 
 variable {S T : Support β}
 
+theorem atoms_eq_of_spec_eq_spec (h : S.spec = T.spec) (A : β ↝ ⊥) :
+    (S ⇘. A)ᴬ.image
+      (λ a ↦ (⟨{i | (S ⇘. A)ᴬ.rel i a}, {i | ∃ N, (S ⇘. A)ᴺ.rel i N ∧ a ∈ Nᴬ}⟩ : AtomCond)) =
+    (T ⇘. A)ᴬ.image
+      (λ a ↦ ⟨{i | (T ⇘. A)ᴬ.rel i a}, {i | ∃ N, (T ⇘. A)ᴺ.rel i N ∧ a ∈ Nᴬ}⟩) :=
+  congr_fun (congr_arg (·ᴬ) h) A
+
+theorem nearLitters_eq_of_spec_eq_spec (h : S.spec = T.spec) (A : β ↝ ⊥) :
+    (S ⇘. A)ᴺ.comp
+      (nearLitterCondRel S A) (nearLitterCondRel_coinjective S A) =
+    (T ⇘. A)ᴺ.comp
+      (nearLitterCondRel T A) (nearLitterCondRel_coinjective T A) :=
+  congr_fun (congr_arg (·ᴺ) h) A
+
+theorem convAtoms_of_spec_eq_spec (h : S.spec = T.spec) {A : β ↝ ⊥} {a b : Atom} :
+    convAtoms S T A a b →
+    (∀ i, (S ⇘. A)ᴬ.rel i a ↔ (T ⇘. A)ᴬ.rel i b) ∧
+    (∀ i, (∃ N, (S ⇘. A)ᴺ.rel i N ∧ a ∈ Nᴬ) ↔ (∃ N, (T ⇘. A)ᴺ.rel i N ∧ b ∈ Nᴬ)) := by
+  rintro ⟨i, ha, hb⟩
+  have := atoms_eq_of_spec_eq_spec h A
+  rw [Enumeration.ext_iff] at this
+  have := (iff_of_eq <| congr_fun₂ this.2 i _).mp ⟨a, ha, rfl⟩
+  obtain ⟨c, hc₁, hc₂⟩ := this
+  rw [AtomCond.mk.injEq] at hc₂
+  cases (T ⇘. A)ᴬ.rel_coinjective.coinjective hb hc₁
+  rw [Set.ext_iff, Set.ext_iff] at hc₂
+  exact ⟨λ x ↦ (hc₂.1 x).symm, λ x ↦ (hc₂.2 x).symm⟩
+
+theorem convNearLitters_of_spec_eq_spec (h : S.spec = T.spec) {A : β ↝ ⊥} {N₁ N₂ : NearLitter} :
+    convNearLitters S T A N₁ N₂ →
+    ∃ c, nearLitterCondRel S A N₁ c ∧ nearLitterCondRel T A N₂ c := by
+  rintro ⟨i, hN₁, hN₂⟩
+  obtain ⟨c, hc⟩ := (nearLitterCondRel_cosurjective S A).cosurjective N₁
+  have := nearLitters_eq_of_spec_eq_spec h A
+  rw [Enumeration.ext_iff] at this
+  have := (iff_of_eq <| congr_fun₂ this.2 i c).mp ⟨N₁, hN₁, hc⟩
+  obtain ⟨N₃, h₁, h₂⟩ := this
+  cases (T ⇘. A)ᴺ.rel_coinjective.coinjective hN₂ h₁
+  cases this
+  exact ⟨c, hc, h₂⟩
+
+theorem atoms_bound_eq_of_spec_eq_spec (h : S.spec = T.spec) (A : β ↝ ⊥) :
+    (S ⇘. A)ᴬ.bound = (T ⇘. A)ᴬ.bound := by
+  have := congr_arg Enumeration.bound (congr_fun (congr_arg (·ᴬ) h) A)
+  exact this
+
+theorem nearLitters_bound_eq_of_spec_eq_spec (h : S.spec = T.spec) (A : β ↝ ⊥) :
+    (S ⇘. A)ᴺ.bound = (T ⇘. A)ᴺ.bound := by
+  have := congr_arg Enumeration.bound (congr_fun (congr_arg (·ᴺ) h) A)
+  exact this
+
 theorem atoms_dom_subset_of_spec_eq_spec (h : S.spec = T.spec) (A : β ↝ ⊥) :
     (S ⇘. A)ᴬ.rel.dom ⊆ (T ⇘. A)ᴬ.rel.dom := by
   rw [← spec_atoms_dom, ← spec_atoms_dom, h]
@@ -266,16 +374,141 @@ theorem nearLitters_dom_subset_of_spec_eq_spec (h : S.spec = T.spec) (A : β ↝
     (S ⇘. A)ᴺ.rel.dom ⊆ (T ⇘. A)ᴺ.rel.dom := by
   rw [← spec_nearLitters_dom, ← spec_nearLitters_dom, h]
 
+theorem convAtoms_injective_of_spec_eq_spec (h : S.spec = T.spec) (A : β ↝ ⊥) :
+    (convAtoms S T A).Injective := by
+  constructor
+  rintro a₁ a₂ b h₁ ⟨i, hai, hbi⟩
+  rw [← (convAtoms_of_spec_eq_spec h h₁).1] at hbi
+  exact (S ⇘. A)ᴬ.rel_coinjective.coinjective hbi hai
+
+theorem atomMemRel_le_of_spec_eq_spec (h : S.spec = T.spec) (A : β ↝ ⊥) :
+    atomMemRel S A ≤ atomMemRel T A := by
+  rintro i j ⟨N, h₁, a, h₂, haS⟩
+  obtain ⟨b, hbT⟩ := atoms_dom_subset_of_spec_eq_spec h A ⟨a, haS⟩
+  obtain ⟨N', h₁', h₂'⟩ := ((convAtoms_of_spec_eq_spec h ⟨j, haS, hbT⟩).2 i).mp ⟨N, h₁, h₂⟩
+  exact ⟨N', h₁', b, h₂', hbT⟩
+
+theorem inflexible_of_inflexible_of_spec_eq_spec (h : S.spec = T.spec) {A : β ↝ ⊥}
+    {N₁ N₂ : NearLitter} :
+    convNearLitters S T A N₁ N₂ → ∀ (P : InflexiblePath β) (t : Tangle P.δ),
+      A = P.A ↘ P.hε ↘. → N₁ᴸ = fuzz P.hδε t → ∃ ρ : AllPerm P.δ, N₂ᴸ = fuzz P.hδε (ρ • t) := by
+  intro hN P t hA ht
+  obtain ⟨c, hN₁, hN₂⟩ := convNearLitters_of_spec_eq_spec h hN
+  obtain (⟨hN₁, _⟩ | ⟨P', t', hA', ht', rfl⟩) := hN₁
+  · cases hN₁ ⟨P, t, hA, ht⟩
+  cases inflexiblePath_subsingleton hA hA' ht ht'
+  cases fuzz_injective (ht.symm.trans ht')
+  clear hA' ht'
+  obtain ⟨t', -, ht', hχ, h₁, h₂⟩ := nearLitterCondRel_inflex hN₂
+  rw [Tangle.code_eq_code_iff] at hχ
+  obtain ⟨ρ, rfl⟩ := hχ
+  exact ⟨ρ, ht'⟩
+
+theorem litter_eq_of_flexible_of_spec_eq_spec (h : S.spec = T.spec) {A : β ↝ ⊥}
+    {N₁ N₂ N₃ N₄ : NearLitter} :
+    convNearLitters S T A N₁ N₂ → convNearLitters S T A N₃ N₄ →
+    ¬Inflexible A N₁ᴸ → ¬Inflexible A N₂ᴸ → ¬Inflexible A N₃ᴸ → ¬Inflexible A N₄ᴸ →
+    N₁ᴸ = N₃ᴸ → N₂ᴸ = N₄ᴸ := by
+  intro h₁₂ h₃₄ h₁ h₂ _ _ h₁₃
+  obtain ⟨c, hN₁, hN₂⟩ := convNearLitters_of_spec_eq_spec h h₁₂
+  obtain (⟨-, rfl⟩ | hN₁) := hN₁
+  swap
+  · cases h₁ (inflexible_of_mem_dom_nearLitterCondInflexRel ⟨c, hN₁⟩)
+  obtain (⟨-, h⟩ | hN₂) := hN₂
+  swap
+  · cases h₂ (inflexible_of_mem_dom_nearLitterCondInflexRel ⟨_, hN₂⟩)
+  rw [NearLitterCond.flex.injEq, FlexCond.mk.injEq, Set.ext_iff] at h
+  obtain ⟨i, hi₁, hi₂⟩ := h₃₄
+  obtain ⟨N', hN'₁, hN'₂⟩ := (h i).mp ⟨N₃, hi₁, h₁₃⟩
+  cases (T ⇘. A)ᴺ.rel_coinjective.coinjective hi₂ hN'₁
+  exact hN'₂
+
+theorem convAtoms_of_inflexible_of_spec_eq_spec (h : S.spec = T.spec) (A : β ↝ ⊥)
+    (N₁ N₂ : NearLitter) (P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) :
+    A = P.A ↘ P.hε ↘. → N₁ᴸ = fuzz P.hδε t → N₂ᴸ = fuzz P.hδε (ρ • t) →
+    convNearLitters S T A N₁ N₂ → ∀ (B : P.δ ↝ ⊥),
+      (convAtoms (S ⇘ (P.A ↘ P.hδ)) (T ⇘ (P.A ↘ P.hδ)) B ⊓ λ a _ ↦ a ∈ (t.support ⇘. B)ᴬ) ≤
+      λ a b ↦ b = ρᵁ ⇘. B • a := by
+  rintro hA ht₁ ht₂ hN B a b ⟨hab, ha⟩
+  obtain ⟨c, h₁, h₂⟩ := convNearLitters_of_spec_eq_spec h hN
+  obtain (⟨h₁, -⟩ | ⟨P', t', hA', ht', rfl⟩) := h₁
+  · cases h₁ ⟨P, t, hA, ht₁⟩
+  cases inflexiblePath_subsingleton hA hA' ht₁ ht'
+  cases fuzz_injective (ht₁.symm.trans ht')
+  clear hA' ht'
+  obtain ⟨t', -, hN₂, -, hBa, hBN⟩ := nearLitterCondRel_inflex h₂
+  cases fuzz_injective (ht₂.symm.trans hN₂)
+  obtain ⟨i, hi₁, hi₂⟩ := hab
+  obtain ⟨j, hj⟩ := ha
+  obtain ⟨b', hb'₁, hb'₂⟩ := (iff_of_eq <| congr_fun₃ hBa B i j).mp ⟨a, hi₁, hj⟩
+  cases (Enumeration.rel_coinjective _).coinjective hi₂ hb'₁
+  rw [Tangle.smul_support, smul_derivBot, BaseSupport.smul_atoms] at hb'₂
+  cases (t.support ⇘. B)ᴬ.rel_coinjective.coinjective hj hb'₂
+  rw [Tree.botDeriv_eq, smul_inv_smul]
+
+theorem convNearLitters_of_inflexible_of_spec_eq_spec (h : S.spec = T.spec) (A : β ↝ ⊥)
+    (N₁ N₂ : NearLitter) (P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) :
+    A = P.A ↘ P.hε ↘. → N₁ᴸ = fuzz P.hδε t → N₂ᴸ = fuzz P.hδε (ρ • t) →
+    convNearLitters S T A N₁ N₂ → ∀ (B : P.δ ↝ ⊥),
+      (convNearLitters (S ⇘ (P.A ↘ P.hδ)) (T ⇘ (P.A ↘ P.hδ)) B ⊓ λ N _ ↦ N ∈ (t.support ⇘. B)ᴺ) ≤
+      λ N₁' N₂' ↦ N₂' = ρᵁ ⇘. B • N₁' := by
+  rintro hA ht₁ ht₂ hN B N₁' N₂' ⟨hab, ha⟩
+  obtain ⟨c, h₁, h₂⟩ := convNearLitters_of_spec_eq_spec h hN
+  obtain (⟨h₁, -⟩ | ⟨P', t', hA', ht', rfl⟩) := h₁
+  · cases h₁ ⟨P, t, hA, ht₁⟩
+  cases inflexiblePath_subsingleton hA hA' ht₁ ht'
+  cases fuzz_injective (ht₁.symm.trans ht')
+  clear hA' ht'
+  obtain ⟨t', -, hN₂, -, hBa, hBN⟩ := nearLitterCondRel_inflex h₂
+  cases fuzz_injective (ht₂.symm.trans hN₂)
+  obtain ⟨i, hi₁, hi₂⟩ := hab
+  obtain ⟨j, hj⟩ := ha
+  obtain ⟨N₃', hN'₁, hN'₂⟩ := (iff_of_eq <| congr_fun₃ hBN B i j).mp ⟨N₁', hi₁, hj⟩
+  cases (Enumeration.rel_coinjective _).coinjective hi₂ hN'₁
+  rw [Tangle.smul_support, smul_derivBot, BaseSupport.smul_nearLitters] at hN'₂
+  cases (t.support ⇘. B)ᴺ.rel_coinjective.coinjective hj hN'₂
+  rw [Tree.botDeriv_eq, smul_inv_smul]
+
 theorem sameSpecLe_of_spec_eq_spec (h : S.spec = T.spec) :
     SameSpecLE S T where
+  atoms_bound_eq := atoms_bound_eq_of_spec_eq_spec h
+  nearLitters_bound_eq := nearLitters_bound_eq_of_spec_eq_spec h
   atoms_dom_subset := atoms_dom_subset_of_spec_eq_spec h
   nearLitters_dom_subset := nearLitters_dom_subset_of_spec_eq_spec h
-  convAtoms_injective := sorry
-  atomMemRel_le := sorry
-  inflexible_of_inflexible := sorry
-  litter_eq_of_flexible := sorry
-  convAtoms_of_inflexible := sorry
-  convNearLitters_of_inflexible := sorry
+  convAtoms_injective := convAtoms_injective_of_spec_eq_spec h
+  atomMemRel_le := atomMemRel_le_of_spec_eq_spec h
+  inflexible_of_inflexible := inflexible_of_inflexible_of_spec_eq_spec h
+  litter_eq_of_flexible := litter_eq_of_flexible_of_spec_eq_spec h
+  convAtoms_of_inflexible := convAtoms_of_inflexible_of_spec_eq_spec h
+  convNearLitters_of_inflexible := convNearLitters_of_inflexible_of_spec_eq_spec h
+
+theorem atoms_eq_of_sameSpec (h : SameSpec S T) {A : β ↝ ⊥} {i : κ} {a b : Atom}
+    (ha : (S ⇘. A)ᴬ.rel i a) (hb : (T ⇘. A)ᴬ.rel i b) :
+    {i | (T ⇘. A)ᴬ.rel i b} = {i | (S ⇘. A)ᴬ.rel i a} := by
+  ext j : 1
+  constructor
+  · intro hj
+    rw [Set.mem_setOf_eq] at hj
+    have hdom := h.atoms_dom_eq A
+    rw [Set.ext_iff] at hdom
+    obtain ⟨c, hc⟩ := (hdom j).mpr ⟨b, hj⟩
+    cases (h.convAtoms_oneOne A).injective ⟨i, ha, hb⟩ ⟨j, hc, hj⟩
+    exact hc
+  · sorry
+
+theorem spec_le_spec_of_sameSpec (h : SameSpec S T) :
+    S.spec ≤ T.spec := by
+  intro A
+  simp only [spec_atoms, spec_nearLitters]
+  refine ⟨h.atoms_bound_eq A, ?_, h.nearLitters_bound_eq A, ?_⟩
+  · rintro i _ ⟨a, ha, rfl⟩
+    have hdom := h.atoms_dom_eq A
+    rw [Set.ext_iff] at hdom
+    obtain ⟨b, hb⟩ := (hdom i).mp ⟨a, ha⟩
+    refine ⟨b, hb, ?_⟩
+    rw [AtomCond.mk.injEq]
+    exact ⟨atoms_eq_of_sameSpec h ha hb, sorry⟩
+  · sorry
 
 theorem spec_eq_spec_iff (S T : Support β) :
     S.spec = T.spec ↔ SameSpec S T := by
diff --git a/ConNF/Setup/Enumeration.lean b/ConNF/Setup/Enumeration.lean
index d9bb0d0259..fc85a48bd7 100644
--- a/ConNF/Setup/Enumeration.lean
+++ b/ConNF/Setup/Enumeration.lean
@@ -40,6 +40,11 @@ theorem mem_iff (x : X) (E : Enumeration X) :
     x ∈ E ↔ x ∈ E.rel.codom :=
   Iff.rfl
 
+theorem mem_congr {E F : Enumeration X} (h : E = F) :
+    ∀ x, x ∈ E ↔ x ∈ F := by
+  intro x
+  rw [h]
+
 theorem dom_small (E : Enumeration X) :
     Small E.rel.dom :=
   (iio_small E.bound).mono E.lt_bound
@@ -180,6 +185,11 @@ def image (E : Enumeration X) (f : X → Y) : Enumeration Y where
     rintro i _ _ ⟨x₁, hx₁, rfl⟩ ⟨x₂, hx₂, rfl⟩
     rw [E.rel_coinjective.coinjective hx₁ hx₂]
 
+@[simp]
+theorem image_bound {f : X → Y} :
+    (E.image f).bound = E.bound :=
+  rfl
+
 theorem image_rel {f : X → Y} (i : κ) (y : Y) :
     (E.image f).rel i y ↔ ∃ x, E.rel i x ∧ f x = y :=
   Iff.rfl