diff --git a/ConNF.lean b/ConNF.lean
index 390e661252..e327ea79fa 100644
--- a/ConNF.lean
+++ b/ConNF.lean
@@ -4,4 +4,3 @@ import ConNF.Structural
 import ConNF.Fuzz
 import ConNF.NewTangle
 import ConNF.Foa
-import ConNF.Counting
diff --git a/ConNF/Counting.lean b/ConNF/Counting.lean
deleted file mode 100644
index 70bad5bf2f..0000000000
--- a/ConNF/Counting.lean
+++ /dev/null
@@ -1,11 +0,0 @@
-import ConNF.Counting.OrdSupport
-import ConNF.Counting.CodingFunction
-import ConNF.Counting.Spec
-import ConNF.Counting.SpecSame
-import ConNF.Counting.OrdSupportOrbit
-import ConNF.Counting.OrdSupportOrbitEquiv
-import ConNF.Counting.OrdSupportExtend
-import ConNF.Counting.CountCodingFunction
-import ConNF.Counting.CountSpec
-import ConNF.Counting.CountRaisedSingleton
-import ConNF.Counting.CountTangles
diff --git a/ConNF/Counting/CodingFunction.lean b/ConNF/Counting/CodingFunction.lean
deleted file mode 100644
index fc51098c23..0000000000
--- a/ConNF/Counting/CodingFunction.lean
+++ /dev/null
@@ -1,166 +0,0 @@
-import ConNF.Counting.OrdSupport
-
-/-!
-# Coding functions
--/
-
-open MulAction Set Sum
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions] [FoaAssumptions α] {β : Iic α}
-
-structure CodingFunction (β : Iic α) where
-  decode : OrdSupport β →. Tangle β
-  dom_nonempty : decode.Dom.Nonempty
-  supports_decode' (S : OrdSupport β) (hS : (decode S).Dom) :
-    Supports (Allowable β) (S : Set (SupportCondition β)) ((decode S).get hS)
-  dom_iff (S T : OrdSupport β) (hS : (decode S).Dom) :
-    (decode T).Dom ↔ ∃ ρ : Allowable β, T = ρ • S
-  decode_smul' (S : OrdSupport β) (ρ : Allowable β)
-    (h₁ : (decode S).Dom) (h₂ : (decode (ρ • S)).Dom) :
-    (decode (ρ • S)).get h₂ = ρ • (decode S).get h₁
-
-namespace CodingFunction
-
-instance : Membership (OrdSupport β) (CodingFunction β) where
-  mem S χ := (χ.decode S).Dom
-
-theorem mem_iff {χ : CodingFunction β} {S : OrdSupport β} :
-    S ∈ χ ↔ (χ.decode S).Dom :=
-  Iff.rfl
-
-theorem mem_iff_of_mem {χ : CodingFunction β} {S T : OrdSupport β} (h : S ∈ χ) :
-    T ∈ χ ↔ ∃ ρ : Allowable β, T = ρ • S :=
-  χ.dom_iff S T h
-
-theorem smul_mem {χ : CodingFunction β} {S : OrdSupport β} (ρ : Allowable β) (h : S ∈ χ) :
-    ρ • S ∈ χ :=
-  (χ.mem_iff_of_mem h).mpr ⟨ρ, rfl⟩
-
-theorem mem_of_smul_mem {χ : CodingFunction β} {S : OrdSupport β} {ρ : Allowable β}
-    (h : ρ • S ∈ χ) : S ∈ χ :=
-  (χ.mem_iff_of_mem h).mpr ⟨ρ⁻¹, by rw [inv_smul_smul]⟩
-
-theorem exists_mem (χ : CodingFunction β) :
-    ∃ S, S ∈ χ :=
-  χ.dom_nonempty
-
-theorem supports_decode {χ : CodingFunction β} (S : OrdSupport β) (hS : S ∈ χ) :
-    Supports (Allowable β) (S : Set (SupportCondition β)) ((χ.decode S).get hS) :=
-  χ.supports_decode' S hS
-
-theorem decode_smul {χ : CodingFunction β} (S : OrdSupport β) (ρ : Allowable β) (h : ρ • S ∈ χ) :
-    (χ.decode (ρ • S)).get h = ρ • (χ.decode S).get (mem_of_smul_mem h) :=
-  χ.decode_smul' S ρ _ _
-
-/-- Two coding functions are equal if they decode a single ordered support to the same tangle. -/
-theorem ext {χ₁ χ₂ : CodingFunction β}
-    (S : OrdSupport β) (h₁ : S ∈ χ₁) (h₂ : S ∈ χ₂)
-    (h : (χ₁.decode S).get h₁ = (χ₂.decode S).get h₂) :
-    χ₁ = χ₂ := by
-  rw [mk.injEq]
-  funext T
-  refine Part.ext' ?_ ?_
-  · rw [← mem_iff, mem_iff_of_mem h₁, ← mem_iff, mem_iff_of_mem h₂]
-  · intros h₁' h₂'
-    rw [← mem_iff, mem_iff_of_mem h₁] at h₁'
-    obtain ⟨ρ, rfl⟩ := h₁'
-    rw [χ₁.decode_smul' S ρ h₁ h₁', χ₂.decode_smul' S ρ h₂ h₂', h]
-
-theorem smul_supports {S : OrdSupport β} {t : Tangle β}
-    (h : Supports (Allowable β) (S : Set (SupportCondition β)) t) (ρ : Allowable β) :
-    Supports (Allowable β) ((ρ • S : OrdSupport β) : Set (SupportCondition β)) (ρ • t) := by
-  intro ρ' hρ'
-  have := h (ρ⁻¹ * ρ' * ρ) ?_
-  · rw [mul_assoc, mul_smul, inv_smul_eq_iff, mul_smul] at this
-    exact this
-  intros c hc
-  rw [mul_assoc, mul_smul, inv_smul_eq_iff, mul_smul]
-  refine hρ' ?_
-  simp only [OrdSupport.mem_carrier_iff, OrdSupport.smul_mem, inv_smul_smul]
-  exact hc
-
-theorem decode_congr {χ : CodingFunction β} {S₁ S₂ : OrdSupport β}
-    {h₁ : S₁ ∈ χ} {h₂ : S₂ ∈ χ} (h : S₁ = S₂) :
-    (χ.decode S₁).get h₁ = (χ.decode S₂).get h₂ := by
-  subst h
-  rfl
-
-/-- Produce a coding function for a given ordered support and tangle it supports. -/
-noncomputable def code (S : OrdSupport β) (t : Tangle β)
-    (h : Supports (Allowable β) (S : Set (SupportCondition β)) t) :
-    CodingFunction β where
-  decode T := ⟨∃ ρ : Allowable β, T = ρ • S, fun hT => hT.choose • t⟩
-  dom_nonempty := ⟨S, 1, by rw [one_smul]⟩
-  supports_decode' T hT := by
-    have := smul_supports h hT.choose
-    rw [← hT.choose_spec] at this
-    exact this
-  dom_iff T U hT := by
-    obtain ⟨ρ, rfl⟩ := hT
-    constructor
-    · rintro ⟨ρ', rfl⟩
-      refine ⟨ρ' * ρ⁻¹, ?_⟩
-      rw [smul_smul, inv_mul_cancel_right]
-    · rintro ⟨ρ', h⟩
-      refine ⟨ρ' * ρ, ?_⟩
-      rw [mul_smul]
-      exact h
-  decode_smul' T ρ h₁ h₂ := by
-    rw [← inv_smul_eq_iff, ← inv_smul_eq_iff, smul_smul, smul_smul]
-    refine h _ ?_
-    intros c hc
-    have := h₂.choose_spec.symm
-    conv_rhs at this => rw [h₁.choose_spec]
-    rw [← inv_smul_eq_iff, ← inv_smul_eq_iff, smul_smul, smul_smul] at this
-    exact OrdSupport.smul_eq_of_smul_eq _ ⟨c, hc⟩ this
-
-@[simp]
-theorem code_decode (S : OrdSupport β) (t : Tangle β)
-    (h : Supports (Allowable β) (S : Set (SupportCondition β)) t) :
-    (code S t h).decode S = Part.some t := by
-  refine Part.ext' ?_ ?_
-  · simp only [Allowable.toStructPerm_smul, Part.some_dom, iff_true]
-    refine ⟨1, ?_⟩
-    simp only [map_one, one_smul]
-  · intros h' _
-    refine h _ ?_
-    intros c hc
-    exact OrdSupport.smul_eq_of_smul_eq _ ⟨c, hc⟩ h'.choose_spec.symm
-
-@[simp]
-theorem mem_code_self {S : OrdSupport β} {t : Tangle β}
-    {h : Supports (Allowable β) (S : Set (SupportCondition β)) t} :
-    S ∈ code S t h :=
-  ⟨1, by rw [one_smul]⟩
-
-@[simp]
-theorem mem_code {S : OrdSupport β} {t : Tangle β}
-    {h : Supports (Allowable β) (S : Set (SupportCondition β)) t} (T : OrdSupport β) :
-    T ∈ code S t h ↔ ∃ ρ : Allowable β, T = ρ • S :=
-  Iff.rfl
-
-/-- Every coding function can be obtained by invoking `code` with an ordered support in its
-domain. -/
-theorem eq_code {χ : CodingFunction β} {S : OrdSupport β} (h : S ∈ χ) :
-    χ = code S ((χ.decode S).get h) (χ.supports_decode S h) := by
-  refine ext S h ?_ ?_
-  · refine ⟨1, ?_⟩
-    rw [one_smul]
-  · simp only [code_decode, Part.get_some]
-
-/-- A coding function is *strong* if it contains a strong support. -/
-def Strong (χ : CodingFunction β) : Prop :=
-  ∃ S : OrdSupport β, S ∈ χ ∧ S.Strong
-
-theorem code_strong {S : OrdSupport β} {t : Tangle β}
-    {h : Supports (Allowable β) (S : Set (SupportCondition β)) t} (hS : S.Strong) :
-    (code S t h).Strong :=
-  ⟨S, mem_code_self, hS⟩
-
-end CodingFunction
-
-end ConNF
diff --git a/ConNF/Counting/CountCodingFunction.lean b/ConNF/Counting/CountCodingFunction.lean
deleted file mode 100644
index 3f5323e608..0000000000
--- a/ConNF/Counting/CountCodingFunction.lean
+++ /dev/null
@@ -1,59 +0,0 @@
-import ConNF.Counting.Recode
-
-/-!
-# Counting coding functions
--/
-
-open Cardinal Function MulAction Set
-open scoped Cardinal
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions] [CountingAssumptions α] {β γ : Iic α} (hγ : γ < β)
-
-noncomputable def recodeSurjection
-    (x : { x : Set (RaisedSingleton hγ) × OrdSupportOrbit β //
-      x.2.Strong ∧
-      ∃ ho : ∀ U ∈ x.2, AppearsRaised hγ (Subtype.val '' x.1) U,
-      ∀ U, ∀ hU : U ∈ x.2,
-        Supports (Allowable β) {c | c ∈ U} (decodeRaised hγ (Subtype.val '' x.1) U (ho U hU)) }) :
-    { χ : CodingFunction β // CodingFunction.Strong χ } :=
-  ⟨raisedCodingFunction hγ (Subtype.val '' x.val.1) x.val.2 x.prop.2.1 x.prop.2.2,
-    raisedCodingFunction_strong hγ x.prop.1⟩
-
-theorem recodeSurjection_surjective : Surjective (recodeSurjection hγ) := by
-  rintro ⟨χ, S, hSχ, hS⟩
-  refine ⟨⟨⟨Subtype.val ⁻¹' raiseSingletons hγ S ((χ.decode S).get hSχ), OrdSupportOrbit.mk S⟩,
-      ?_, ?_, ?_⟩, ?_⟩
-  · exact ⟨S, rfl, hS⟩
-  · intro U hU
-    rw [image_preimage_eq_of_subset (raiseSingletons_subset_range hγ)]
-    exact appearsRaised_of_mem_orbit hγ S ((χ.decode S).get hSχ) (χ.supports_decode S hSχ) U hU
-  · intro U hU
-    conv in (Subtype.val '' _) => rw [image_preimage_eq_of_subset (raiseSingletons_subset_range hγ)]
-    exact supports_decodeRaised_of_mem_orbit hγ S
-      ((χ.decode S).get hSχ) (χ.supports_decode S hSχ) U hU
-  · rw [recodeSurjection, Subtype.mk.injEq]
-    conv in (Subtype.val '' _) => rw [image_preimage_eq_of_subset (raiseSingletons_subset_range hγ)]
-    conv_rhs => rw [CodingFunction.eq_code hSχ,
-      ← recode_eq hγ S ((χ.decode S).get hSχ) (χ.supports_decode S hSχ)]
-
-/-- The main lemma about counting strong coding functions. -/
-theorem mk_strong_codingFunction_le :
-    #{ χ : CodingFunction β // χ.Strong } ≤
-    2 ^ #(RaisedSingleton hγ) * #{ o : OrdSupportOrbit β // o.Strong } := by
-  refine (mk_le_of_surjective (recodeSurjection_surjective hγ)).trans ?_
-  refine (mk_subtype_le_of_subset (q := fun x => x.2.Strong) (fun x hx => hx.1)).trans ?_
-  have := mk_prod (Set (RaisedSingleton hγ)) { o : OrdSupportOrbit β // o.Strong }
-  simp only [mk_set, lift_id] at this
-  rw [← this]
-  refine ⟨⟨fun x => ⟨x.val.1, x.val.2, x.prop⟩, ?_⟩⟩
-  rintro ⟨⟨cs₁, o₁⟩, _⟩ ⟨⟨cs₂, o₂⟩, _⟩ h
-  simp only [Prod.mk.injEq, Subtype.mk.injEq] at h
-  cases h.1
-  cases h.2
-  rfl
-
-end ConNF
diff --git a/ConNF/Counting/CountRaisedSingleton.lean b/ConNF/Counting/CountRaisedSingleton.lean
deleted file mode 100644
index 86e2760472..0000000000
--- a/ConNF/Counting/CountRaisedSingleton.lean
+++ /dev/null
@@ -1,35 +0,0 @@
-import ConNF.Counting.Recode
-import ConNF.Counting.Spec
-
-/-!
-# Counting raised singletons
--/
-
-open Cardinal Function MulAction Set
-open scoped Cardinal
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions] [CountingAssumptions α] {β γ : Iic α} (hγ : γ < β)
-
-noncomputable def raisedSingleton_map
-    (σ : Spec β) (hσ : σ.Strong) (χ : CodingFunction γ) (hχ : χ.Strong) :
-    RaisedSingleton hγ :=
-  sorry
-
-theorem raisedSingleton_surjective :
-    Surjective (fun x : { σ : Spec β // σ.Strong } × { χ : CodingFunction γ // χ.Strong } =>
-      ULift.up.{u + 1} <| raisedSingleton_map hγ x.1.1 x.1.2 x.2.1 x.2.2) := sorry
-
-/-- The main lemma about counting raised singletons. -/
-theorem mk_raisedSingleton :
-    lift.{u + 1} #(RaisedSingleton hγ) ≤
-    #{ σ : Spec β // σ.Strong } * lift.{u + 1} #{ χ : CodingFunction γ // χ.Strong } := by
-  have := mk_le_of_surjective (raisedSingleton_surjective hγ)
-  simp only [mk_uLift, mk_prod] at this
-  rw [lift_id'.{u, u + 1} _] at this
-  exact this
-
-end ConNF
diff --git a/ConNF/Counting/CountSpec.lean b/ConNF/Counting/CountSpec.lean
deleted file mode 100644
index 1122c6722c..0000000000
--- a/ConNF/Counting/CountSpec.lean
+++ /dev/null
@@ -1,393 +0,0 @@
-import ConNF.Counting.Recode
-import ConNF.Counting.OrdSupportOrbitEquiv
-
-/-!
-# Counting specifications
--/
-
-open Cardinal Function MulAction Set
-open scoped Cardinal
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions] [FoaAssumptions α] {β γ : Iic α} (hγ : γ < β)
-
-inductive SpecConditionBelow (β : Iic α) (i : Ordinal.{u})
-  | atom (A : ExtendedIndex β) (j : Ordinal) (h : j < i)
-  | flexible (A : ExtendedIndex β)
-  | inflexibleCoe (A : ExtendedIndex β) (h : InflexibleCoePath A)
-      (χ : CodingFunction (h.δ : Iic α)) (hχ : χ.Strong)
-  | inflexibleBot (A : ExtendedIndex β) (h : InflexibleBotPath A) (j : Ordinal) (hj : j < i)
-
-def SpecConditionBelowType (β : Iic α) (i : Ordinal.{u}) :=
-    (ExtendedIndex β × Iio i) ⊕ (ExtendedIndex β) ⊕
-    (ExtendedIndex β × (δ : { δ : Iic α // δ < β }) × { χ : CodingFunction δ.val // χ.Strong }) ⊕
-    (ExtendedIndex β × Iio i)
-
-def specConditionBelow_map {β : Iic α} {i : Ordinal} :
-    SpecConditionBelow β i → SpecConditionBelowType β i
-  | .atom A j hj => Sum.inl (A, ⟨j, hj⟩)
-  | .flexible A => Sum.inr (Sum.inl A)
-  | .inflexibleCoe A h χ hχ => Sum.inr (Sum.inr (Sum.inl
-      (A, ⟨⟨h.δ, h.hδ.trans_le (WithBot.coe_le_coe.mp <| le_of_path h.B)⟩, χ, hχ⟩)))
-  | .inflexibleBot A _ j hj => Sum.inr (Sum.inr (Sum.inr (A, ⟨j, hj⟩)))
-
-theorem specConditionBelow_map_injective {β : Iic α} {i : Ordinal} :
-    Function.Injective (specConditionBelow_map (β := β) (i := i)) := by
-  intro c d h
-  unfold specConditionBelow_map at h
-  cases c with
-  | atom A j h =>
-    cases d <;> cases h
-    rfl
-  | flexible A =>
-    cases d <;> cases h
-    rfl
-  | inflexibleCoe A P χ hχ =>
-    cases d with
-    | inflexibleCoe B Q χ' hχ' =>
-      rw [Sum.inr.inj_iff, Sum.inr.inj_iff, Sum.inl.inj_iff] at h
-      simp only [Prod.mk.injEq, Sigma.mk.inj_iff, Subtype.mk.injEq] at h
-      have := (P.hA).symm.trans (h.1.trans Q.hA)
-      obtain ⟨⟨γ, _⟩, ⟨δ, _⟩, ⟨ε, _⟩, _⟩ := P
-      obtain ⟨⟨γ', _⟩, ⟨δ', _⟩, ⟨ε', _⟩, _⟩ := Q
-      have := Quiver.Path.obj_eq_of_cons_eq_cons this
-      rw [WithBot.coe_inj] at this
-      subst this
-      have := eq_of_heq (Quiver.Path.heq_of_cons_eq_cons this)
-      have := Quiver.Path.obj_eq_of_cons_eq_cons this
-      rw [WithBot.coe_inj] at this
-      subst this
-      have := eq_of_heq (Quiver.Path.heq_of_cons_eq_cons this)
-      subst this
-      cases h.1
-      cases h.2.1
-      cases h.2.2
-      rfl
-    | _ => try cases h
-  | inflexibleBot A P j hj =>
-    cases d with
-    | inflexibleBot B Q χ' hχ' =>
-      rw [Sum.inr.inj_iff, Sum.inr.inj_iff, Sum.inr.inj_iff] at h
-      simp only [Prod.mk.injEq, Sigma.mk.inj_iff, Subtype.mk.injEq] at h
-      have := (P.hA).symm.trans (h.1.trans Q.hA)
-      obtain ⟨⟨γ, _⟩, ⟨ε, _⟩, _⟩ := P
-      obtain ⟨⟨γ', _⟩, ⟨ε', _⟩, _⟩ := Q
-      have := Quiver.Path.obj_eq_of_cons_eq_cons this
-      rw [WithBot.coe_inj] at this
-      subst this
-      have := eq_of_heq (Quiver.Path.heq_of_cons_eq_cons this)
-      have := Quiver.Path.obj_eq_of_cons_eq_cons this
-      rw [WithBot.coe_inj] at this
-      subst this
-      have := eq_of_heq (Quiver.Path.heq_of_cons_eq_cons this)
-      subst this
-      cases h.1
-      cases h.2
-      rfl
-    | _ => try cases h
-
-instance {α : Type _} {x : α} : IsTrichotomous ({x} : Set α) emptyRelation := by
-  constructor
-  rintro ⟨_, rfl⟩ ⟨_, rfl⟩
-  exact Or.inr (Or.inl rfl)
-
-instance {α : Type _} {x : α} : IsTrans ({x} : Set α) emptyRelation := by
-  constructor
-  rintro ⟨_, rfl⟩ ⟨_, rfl⟩ _ h _
-  cases h
-
-instance {α : Type _} {x : α} : IsWellFounded ({x} : Set α) emptyRelation := emptyWf.isWellFounded
-
-instance {α : Type _} {x : α} : IsWellOrder ({x} : Set α) emptyRelation := ⟨⟩
-
-def OrdSupport.litter (β : Iic α) (L : Litter) : OrdSupport β where
-  carrier := {⟨Quiver.Hom.toPath (WithBot.bot_lt_coe β.val), Sum.inr L.toNearLitter⟩}
-  carrier_small := small_singleton _
-  r := emptyRelation
-  r_isWellOrder := inferInstance
-
-theorem OrdSupport.litter_supports (β : Iic α) (L : Litter) :
-    Supports (Allowable β) (OrdSupport.litter β L).carrier
-      (typedNearLitter (Litter.toNearLitter L) : Tangle β) := by
-  intro ρ h
-  have := h rfl
-  simp only [Allowable.smul_supportCondition_eq_iff, Sum.smul_inr, Sum.inr.injEq] at this
-  rw [Allowable.smul_typedNearLitter, this]
-
-theorem OrdSupport.litter_strong (β : Iic α) (L : Litter)
-    (hL : Flexible α (Quiver.Hom.toPath (WithBot.bot_lt_coe β.val)) L) :
-    (OrdSupport.litter β L).Strong := by
-  constructor
-  · rintro ⟨_, rfl⟩
-    exact Reduced.mkLitter _
-  · rintro c ⟨_, rfl⟩ _ hcd
-    cases not_transConstrains_flexible α c hL hcd
-  · rintro c ⟨_, rfl⟩ hcd
-    cases not_transConstrains_flexible α c hL hcd
-
-noncomputable def CodingFunction.codeLitter (β : Iic α) (L : Litter) : CodingFunction β :=
-  CodingFunction.code
-    (OrdSupport.litter β L)
-    (typedNearLitter L.toNearLitter)
-    (OrdSupport.litter_supports β L)
-
-theorem CodingFunction.codeLitter_strong (β : Iic α) (L : Litter)
-    (hL : Flexible α (Quiver.Hom.toPath (WithBot.bot_lt_coe β.val)) L) :
-    (CodingFunction.codeLitter β L).Strong :=
-  CodingFunction.code_strong (OrdSupport.litter_strong β L hL)
-
-theorem mk_codingFunction_ne_zero (β : Iic α) :
-    #{ χ : CodingFunction β // χ.Strong } ≠ 0 := by
-  have := (aleph0_pos.trans_le μ_isStrongLimit.isLimit.aleph0_le).ne.symm
-  rw [← mk_flexible α (Quiver.Hom.toPath (WithBot.bot_lt_coe β.val))] at this
-  rw [mk_ne_zero_iff] at this ⊢
-  obtain ⟨L, hL⟩ := this
-  exact ⟨CodingFunction.codeLitter β L, CodingFunction.codeLitter_strong β L hL⟩
-
-theorem sum_mk_codingFunction_ne_zero (β : Iic α) (hβ : ¬IsMin β) :
-    (sum fun δ : { δ : Iic α // δ < β } =>
-      lift.{u + 1} #{ χ : CodingFunction δ.val // χ.Strong }) ≠ 0 := by
-  rw [not_isMin_iff] at hβ
-  obtain ⟨δ, hδ⟩ := hβ
-  intro h
-  rw [← lift_sum, lift_eq_zero, ← mk_sigma, mk_eq_zero_iff] at h
-  refine h.false ⟨⟨δ, hδ⟩, ?_⟩
-  have := mk_codingFunction_ne_zero δ
-  rw [mk_ne_zero_iff] at this
-  exact this.some
-
-theorem _root_.Cardinal.mul_le_of_le {a b c : Cardinal} (ha : a ≤ c) (hb : b ≤ c) (hc : ℵ₀ ≤ c) :
-    a * b ≤ c := by
-  by_cases ha' : ℵ₀ ≤ a
-  · refine le_trans (mul_le_max_of_aleph0_le_left ha') ?_
-    simp only [ge_iff_le, max_le_iff]
-    exact ⟨ha, hb⟩
-  by_cases hb' : ℵ₀ ≤ b
-  · refine le_trans (mul_le_max_of_aleph0_le_right hb') ?_
-    simp only [ge_iff_le, max_le_iff]
-    exact ⟨ha, hb⟩
-  · simp only [not_le] at ha' hb'
-    exact (mul_lt_aleph0 ha' hb').le.trans hc
-
-@[simp]
-theorem mk_iio (i : Ordinal.{u}) : #(Iio i) = lift.{u + 1} i.card :=
-  Ordinal.mk_initialSeg i
-
-theorem mk_specConditionBelow (β : Iic α) (hβ : ¬IsMin β)
-    (i : Ordinal.{u}) (hi : i.card ≤ #κ) :
-    #(SpecConditionBelow β i) ≤
-    lift.{u + 1}
-      (#κ * sum fun δ : { δ : Iic α // δ < β } => #{ χ : CodingFunction δ.val // χ.Strong }) := by
-  have : #(SpecConditionBelow β i) ≤ #(SpecConditionBelowType β i) :=
-    ⟨specConditionBelow_map, specConditionBelow_map_injective⟩
-  refine le_trans this ?_
-  rw [SpecConditionBelowType]
-  simp only [mk_sum, mk_prod, lift_id, mk_sigma, lift_mul, lift_sum, lift_lift, lift_add]
-  have : ℵ₀ ≤ lift.{u + 1} #κ *
-      sum fun δ : { δ : Iic α // δ < β } => lift.{u + 1} #{ χ : CodingFunction δ.val // χ.Strong }
-  · rw [aleph0_le_mul_iff]
-    simp only [ne_eq, lift_eq_zero, mk_ne_zero, not_false_eq_true, aleph0_le_lift, aleph0_le_mk,
-      true_or, and_true, true_and]
-    exact sum_mk_codingFunction_ne_zero β hβ
-  refine add_le_of_le this ?_ (add_le_of_le this ?_ (add_le_of_le this ?_ ?_))
-  · refine le_trans ?_ (le_mul_right (sum_mk_codingFunction_ne_zero β hβ))
-    refine mul_le_of_le ?_ ?_ ?_
-    · rw [lift_le]
-      exact (mk_extendedIndex β).trans Λ_lt_κ.le
-    · rw [mk_iio, Ordinal.lift_card, Ordinal.lift_card, Ordinal.lift_lift,
-        ← Ordinal.lift_card, lift_le]
-      exact hi
-    · simp only [aleph0_le_lift, aleph0_le_mk]
-  · refine le_trans ?_ (le_mul_right (sum_mk_codingFunction_ne_zero β hβ))
-    rw [lift_le]
-    exact (mk_extendedIndex β).trans Λ_lt_κ.le
-  · refine mul_le_mul' ?_ le_rfl
-    rw [lift_le]
-    exact (mk_extendedIndex β).trans Λ_lt_κ.le
-  · refine le_trans ?_ (le_mul_right (sum_mk_codingFunction_ne_zero β hβ))
-    refine mul_le_of_le ?_ ?_ ?_
-    · rw [lift_le]
-      exact (mk_extendedIndex β).trans Λ_lt_κ.le
-    · rw [mk_iio, Ordinal.lift_card, Ordinal.lift_card, Ordinal.lift_lift,
-        ← Ordinal.lift_card, lift_le]
-      exact hi
-    · simp only [aleph0_le_lift, aleph0_le_mk]
-
-theorem orderType_lt_of_specifies (σ : Spec β) (S : OrdSupport β) (hσS : σ.Specifies S) :
-    σ.orderType.card < #κ := by
-  rw [Spec.orderType_eq_of_specifies hσS]
-  exact S.small
-
--- TODO: Could rewrite `SpecSame` making much bigger use of `specifies_subsingleton`.
-
-def SpecType (β : Iic α) : Type _ :=
-  (i : Iio (#κ).ord) × (Iio i.val → SpecConditionBelow β i)
-
-theorem specCondition_atom_below {β : Iic α}
-    {σ : { σ : Spec β // σ.Strong }}
-    {i j : Ordinal} {hi : i < σ.val.orderType} {A : ExtendedIndex β}
-    (h : SpecCondition.atom A j = σ.val.cond i hi) :
-    j < σ.val.orderType := by
-  obtain ⟨σ, S, hS, hσS⟩ := σ
-  cases Spec.specifies_subsingleton S hσS (Spec.spec_specifies hS)
-  simp only [Spec.spec_cond_eq, Spec.specCondition] at h
-  set c := S.conditionAt i hi
-  obtain ⟨⟨B, a | N⟩, hc⟩ := c
-  · simp only [OrdSupport.coe_sort_coe, SpecCondition.atom.injEq] at h
-    cases h.1
-    cases h.2
-    exact Ordinal.typein_lt_type S.r _
-  · dsimp only at h
-    split_ifs at h
-
-theorem specCondition_inflexibleBot_below {β : Iic α}
-    {σ : { σ : Spec β // σ.Strong }}
-    {i j : Ordinal} {hi : i < σ.val.orderType} {A : ExtendedIndex β} {h : InflexibleBotPath A}
-    (h : SpecCondition.inflexibleBot A h j = σ.val.cond i hi) :
-    j < σ.val.orderType := by
-  obtain ⟨σ, S, hS, hσS⟩ := σ
-  cases Spec.specifies_subsingleton S hσS (Spec.spec_specifies hS)
-  simp only [Spec.spec_cond_eq, Spec.specCondition] at h
-  set c := S.conditionAt i hi
-  obtain ⟨⟨B, a | N⟩, hc⟩ := c
-  · simp only at h
-  · dsimp only at h
-    split_ifs at h
-    simp only [OrdSupport.coe_sort_coe, SpecCondition.inflexibleBot.injEq] at h
-    cases h.2.2
-    exact Ordinal.typein_lt_type S.r _
-
-noncomputable def specCondition_map (β : Iic α) (σ : { σ : Spec β // σ.Strong })
-    (i : Iio σ.val.orderType) : SpecConditionBelow β (σ.val.orderType) :=
-  (σ.val.cond i i.prop).rec
-  (motive := fun c => c = σ.val.cond i i.prop → SpecConditionBelow β (σ.val.orderType))
-  (fun A j hc => .atom A j (specCondition_atom_below hc))
-  (fun A _ => .flexible A)
-  (fun A h χ hχ _ => .inflexibleCoe A h χ hχ)
-  (fun A h j hc => .inflexibleBot A h j (specCondition_inflexibleBot_below hc))
-  rfl
-
-theorem specCondition_map_mk_congr {β : Iic α} {o : Ordinal}
-    {cond : (i : Ordinal) → i < o → SpecCondition β} {h : Spec.Strong ⟨o, cond⟩}
-    {i : Ordinal} {hi : i < o} {d : SpecCondition β} (hd : d = cond i hi) :
-    specCondition_map β ⟨⟨o, cond⟩, h⟩ ⟨i, hi⟩ =
-    d.rec
-    (motive := fun c => c = cond i hi → SpecConditionBelow β o)
-    (fun A j hc => .atom A j (specCondition_atom_below (σ := ⟨⟨o, cond⟩, h⟩) hc))
-    (fun A _ => .flexible A)
-    (fun A h χ hχ _ => .inflexibleCoe A h χ hχ)
-    (fun A h' j hc => .inflexibleBot A h' j
-      (specCondition_inflexibleBot_below (σ := ⟨⟨o, cond⟩, h⟩) hc))
-    hd := by
-  subst hd
-  rfl
-
-noncomputable def specType_map (β : Iic α) (σ : { σ : Spec β // σ.Strong }) :
-    SpecType β :=
-  ⟨⟨σ.val.orderType,
-    lt_ord.mpr (orderType_lt_of_specifies σ.val σ.prop.choose σ.prop.choose_spec.2)⟩,
-    specCondition_map β σ⟩
-
-theorem specType_map_injective (β : Iic α) : Injective (specType_map β) := by
-  rintro ⟨⟨o₁, c₁⟩, S₁, hS₁, hσS₁⟩ ⟨⟨σ₂, c₂⟩, S₂, hS₂, hσS₂⟩ h
-  rw [specType_map, specType_map, Sigma.ext_iff] at h
-  cases h.1
-  simp only [heq_eq_eq, true_and] at h
-  simp only [Subtype.mk.injEq, Spec.mk.injEq, heq_eq_eq, true_and]
-  funext i hi
-  have := congr_fun h ⟨i, hi⟩
-  set d₁ := c₁ i hi with hd₁
-  set d₂ := c₂ i hi with hd₂
-  revert hd₁ hd₂
-  cases d₁ with
-  | atom =>
-    cases d₂ <;>
-      intros hd₁ hd₂ <;>
-      rw [specCondition_map_mk_congr hd₁, specCondition_map_mk_congr hd₂] at this <;>
-      aesop
-  | flexible =>
-    cases d₂ <;>
-      intros hd₁ hd₂ <;>
-      rw [specCondition_map_mk_congr hd₁, specCondition_map_mk_congr hd₂] at this <;>
-      aesop
-  | inflexibleCoe =>
-    cases d₂ with
-    | inflexibleCoe =>
-      intros hd₁ hd₂
-      rw [specCondition_map_mk_congr hd₁, specCondition_map_mk_congr hd₂,
-        SpecConditionBelow.inflexibleCoe.injEq] at this
-      cases this.1
-      cases eq_of_heq this.2.1
-      cases eq_of_heq this.2.2
-      rfl
-    | _ =>
-      intros hd₁ hd₂
-      rw [specCondition_map_mk_congr hd₁, specCondition_map_mk_congr hd₂] at this
-      aesop
-  | inflexibleBot =>
-    cases d₂ with
-    | inflexibleBot =>
-      intros hd₁ hd₂
-      rw [specCondition_map_mk_congr hd₁, specCondition_map_mk_congr hd₂,
-        SpecConditionBelow.inflexibleBot.injEq] at this
-      cases this.1
-      cases eq_of_heq this.2.1
-      cases this.2.2
-      rfl
-    | _ =>
-      intros hd₁ hd₂
-      rw [specCondition_map_mk_congr hd₁, specCondition_map_mk_congr hd₂] at this
-      aesop
-
-theorem Cardinal.power_le_power_left {a b c : Cardinal} : a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c := by
-  refine Cardinal.inductionOn₃ a b c ?_
-  rintro α β γ hα ⟨f⟩
-  by_cases hβ : Nonempty β
-  · rw [power_def, power_def]
-    refine ⟨fun g x => g (Function.invFun f x), ?_⟩
-    intro g₁ g₂ h
-    funext x
-    have h₁ := congr_fun h (f x)
-    have h₂ := congr_fun (Function.invFun_comp f.injective) x
-    dsimp only [comp_apply] at h₁ h₂
-    rw [h₂] at h₁
-    exact h₁
-  rw [mk_ne_zero_iff] at hα
-  rw [not_nonempty_iff] at hβ
-  rw [power_def, power_def]
-  refine ⟨fun _ _ => hα.some, ?_⟩
-  intro g₁ g₂ _
-  funext x
-  exact hβ.elim x
-
-/-- The main lemma about counting strong specifications. -/
-theorem mk_spec_le (β : Iic α) (hβ : ¬IsMin β) :
-    #{ σ : Spec β // σ.Strong } ≤
-    lift.{u + 1} (#κ * (2 ^ #κ * (sum fun δ : { δ : Iic α // δ < β } =>
-        #{ χ : CodingFunction δ.val // χ.Strong }) ^ #κ)) := by
-  refine (mk_le_of_injective (specType_map_injective β)).trans ?_
-  rw [SpecType]
-  simp only [mk_sigma, mk_pi, prod_const, mk_iio, lift_id]
-  suffices : ∀ i : (Iio (#κ).ord),
-      #(SpecConditionBelow β i.val) ^ lift.{u + 1} i.val.card ≤
-      lift.{u + 1} (2 ^ #κ * (sum fun δ : { δ : Iic α // δ < β } =>
-        #{ χ : CodingFunction δ.val // χ.Strong }) ^ #κ)
-  · refine (sum_le_sum _ _ this).trans ?_
-    simp only [sum_const, mk_iio, card_ord, lift_id, lift_mul]
-    rfl
-  rintro ⟨i, hi⟩
-  have := mk_specConditionBelow β hβ i (lt_ord.mp hi).le
-  refine (power_le_power_right (c := lift.{u + 1} i.card) this).trans ?_
-  rw [← lift_power, lift_le, mul_power]
-  refine mul_le_mul' ?_ ?_
-  · rw [← power_self_eq κ_isRegular.aleph0_le]
-    exact power_le_power_left κ_isRegular.pos.ne.symm (lt_ord.mp hi).le
-  · refine power_le_power_left ?_ (lt_ord.mp hi).le
-    have := sum_mk_codingFunction_ne_zero β hβ
-    rw [← lift_sum, ne_eq, lift_eq_zero] at this
-    exact this
-
-end ConNF
diff --git a/ConNF/Counting/CountTangles.lean b/ConNF/Counting/CountTangles.lean
deleted file mode 100644
index 8f193bf72a..0000000000
--- a/ConNF/Counting/CountTangles.lean
+++ /dev/null
@@ -1,20 +0,0 @@
-import ConNF.Counting.CountCodingFunction
-import ConNF.Counting.CountSpec
-import ConNF.Counting.CountRaisedSingleton
-
-/-!
-# Counting tangles
--/
-
-open Cardinal Function MulAction Set
-open scoped Cardinal
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions] [CountingAssumptions α] {β γ : Iic α} (hγ : γ < β)
-
-
-
-end ConNF
diff --git a/ConNF/Counting/Hypotheses.lean b/ConNF/Counting/Hypotheses.lean
deleted file mode 100644
index 48f31204ae..0000000000
--- a/ConNF/Counting/Hypotheses.lean
+++ /dev/null
@@ -1,51 +0,0 @@
-import ConNF.Structural.Pretangle
-import ConNF.Foa.Basic.Reduction
-
-/-!
-# Hypotheses
--/
-
-open MulAction Quiver Set Sum WithBot
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions]
-
-class CountingAssumptions (α : Λ) [BasePositions] extends FoaAssumptions α where
-  toPretangle (β : IicBot α) : Tangle β → Pretangle β
-  toPretangle_smul (β : IicBot α) (ρ : Allowable β) (t : Tangle β) :
-    toPretangle β (ρ • t) = ρ • toPretangle β t
-  /-- Tangles contain only tangles. -/
-  eq_toPretangle_of_mem (β : Iic α) (γ : IicBot α) (h : γ < β) (t₁ : Tangle β) (t₂ : Pretangle γ) :
-    t₂ ∈ Pretangle.ofCoe (toPretangle β t₁) γ h → ∃ t₂' : Tangle γ, t₂ = toPretangle γ t₂'
-  /-- Tangles are extensional at every proper level `γ < β`. -/
-  toPretangle_ext (β γ : Iic α) (h : γ < β) (t₁ t₂ : Tangle β) :
-    (∀ t : Pretangle γ,
-      t ∈ Pretangle.ofCoe (toPretangle β t₁) γ (coe_lt_coe.mpr h) ↔
-      t ∈ Pretangle.ofCoe (toPretangle β t₂) γ (coe_lt_coe.mpr h)) →
-    t₁ = t₂
-  /-- Any `γ`-tangle can be treated as a singleton at level `β` if `γ < β`. -/
-  singleton (β : Iic α) (γ : IicBot α) (h : γ < β) (t : Tangle γ) : Tangle β
-  singleton_toPretangle (β : Iic α) (γ : IicBot α) (h : γ < β) (t : Tangle γ) :
-    Pretangle.ofCoe (toPretangle β (singleton β γ h t)) γ h = {toPretangle γ t}
-
-export CountingAssumptions (toPretangle toPretangle_smul eq_toPretangle_of_mem toPretangle_ext
-  singleton singleton_toPretangle)
-
-variable [CountingAssumptions α] {β γ : Iic α} (hγ : γ < β)
-
-theorem singleton_smul (β : Iic α) (γ : Iic α) (h : (γ : IicBot α) < β) (t : Tangle γ)
-    (ρ : Allowable β) :
-    ρ • singleton β γ h t = singleton β γ h (Allowable.comp (Hom.toPath h) ρ • t) := by
-  refine toPretangle_ext β γ ?_ _ _ ?_
-  · simp only [Subtype.mk_lt_mk, coe_lt_coe, Subtype.coe_lt_coe] at h
-    exact h
-  intro u
-  rw [toPretangle_smul, Allowable.toStructPerm_smul, StructPerm.ofCoe_smul,
-    singleton_toPretangle, singleton_toPretangle, smul_set_singleton,
-    mem_singleton_iff, mem_singleton_iff, toPretangle_smul, Allowable.toStructPerm_smul,
-    Allowable.toStructPerm_comp]
-
-end ConNF
diff --git a/ConNF/Counting/OrdSupport.lean b/ConNF/Counting/OrdSupport.lean
deleted file mode 100644
index 53597ca735..0000000000
--- a/ConNF/Counting/OrdSupport.lean
+++ /dev/null
@@ -1,464 +0,0 @@
-import ConNF.Foa.Basic.Reduction
-
-/-!
-# Ordered supports
--/
-
-open Set Sum
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions] [FoaAssumptions α] {β : Iic α}
-
-structure OrdSupport (β : Iic α) where
-  /-- The set of support conditions in this ordered support. -/
-  carrier : Set (SupportCondition β)
-  /-- The carrier set is small. -/
-  carrier_small : Small carrier
-  /-- An order on `carrier`. -/
-  r : carrier → carrier → Prop
-  /-- `r` is a well order. -/
-  r_isWellOrder : IsWellOrder carrier r
-
-namespace OrdSupport
-
-variable {S : OrdSupport β}
-
-instance : CoeTC (OrdSupport β) (Set (SupportCondition β)) where
-  coe := OrdSupport.carrier
-
-instance : Membership (SupportCondition β) (OrdSupport β) where
-  mem c S := c ∈ S.carrier
-
-@[simp]
-theorem mem_carrier_iff {c : SupportCondition β} : c ∈ S.carrier ↔ c ∈ S :=
-  Iff.rfl
-
-instance : CoeSort (OrdSupport β) (Type _) :=
-  ⟨fun S => { x : SupportCondition β // x ∈ S }⟩
-
-instance : HasSubset (OrdSupport β) where
-  Subset S T := ∀ ⦃c : SupportCondition β⦄, c ∈ S → c ∈ T
-
-@[simp, norm_cast]
-theorem coe_sort_coe (S : OrdSupport β) : ((S : Set (SupportCondition β)) : Type _) = S :=
-  rfl
-
-theorem small (S : OrdSupport β) : Small (S : Set (SupportCondition β)) :=
-  S.carrier_small
-
-instance isWellOrder (S : OrdSupport β) : IsWellOrder S S.r := S.r_isWellOrder
-
-instance : PartialOrder S := partialOrderOfSO S.r
-
-open scoped Classical in
-noncomputable instance : LinearOrder S := linearOrderOfSTO S.r
-
-@[ext]
-theorem ext {S T : OrdSupport β} (h₁ : S ⊆ T) (h₂ : T ⊆ S)
-    (h : ∀ c d : S, c < d ↔ (⟨c, h₁ c.prop⟩ : T) < ⟨d, h₁ d.prop⟩) :
-    S = T := by
-  obtain ⟨S, _, r, _⟩ := S
-  obtain ⟨T, _, s, _⟩ := T
-  cases subset_antisymm (show (S : Set (SupportCondition β)) ⊆ T from h₁) h₂
-  simp only [mk.injEq, heq_eq_eq, true_and]
-  ext c d
-  exact h c d
-
-noncomputable def recursion {motive : S → Sort _} (c : S)
-    (h : (c : S) → ((d : S) → d < c → motive d) → motive c) :
-    motive c :=
-  S.isWellOrder.wf.recursion c h
-
-theorem induction {motive : S → Prop} (c : S)
-    (h : (c : S) → ((d : S) → d < c → motive d) → motive c) :
-    motive c :=
-  S.isWellOrder.wf.induction c h
-
-instance : SMul (Allowable β) (OrdSupport β) where
-  smul ρ S := {
-    carrier := {c | ρ⁻¹ • c ∈ S}
-    carrier_small := Small.preimage (MulAction.injective ρ⁻¹) S.small
-    r := fun c d => (⟨ρ⁻¹ • c.val, c.prop⟩ : S) < ⟨ρ⁻¹ • d.val, d.prop⟩
-    r_isWellOrder := by
-      refine isWellOrder_invImage S.isWellOrder
-        (fun c : {c // ρ⁻¹ • c ∈ S} => ⟨ρ⁻¹ • c.val, c.prop⟩) ?_
-      intros c d h
-      simp only [Subtype.mk.injEq, smul_left_cancel_iff, Subtype.coe_injective.eq_iff] at h
-      exact h
-  }
-
-@[simp]
-theorem smul_mem {ρ : Allowable β} {S : OrdSupport β} {c : SupportCondition β} :
-    c ∈ ρ • S ↔ ρ⁻¹ • c ∈ S :=
-  Iff.rfl
-
-theorem inv_smul_mem {ρ : Allowable β} {S : OrdSupport β} {c : SupportCondition β} :
-    ρ⁻¹ • c ∈ S ↔ c ∈ ρ • S :=
-  smul_mem.symm
-
-theorem smul_mem_smul {ρ : Allowable β} {S : OrdSupport β} {c : SupportCondition β} :
-    ρ • c ∈ ρ • S ↔ c ∈ S := by
-  simp only [smul_mem, inv_smul_smul]
-
-theorem smul_mem_inv {ρ : Allowable β} {S : OrdSupport β} {c : SupportCondition β} :
-    c ∈ ρ⁻¹ • S ↔ ρ • c ∈ S := by
-  simp only [smul_mem, inv_inv]
-
-@[simp]
-theorem lt_iff_smul {ρ : Allowable β} {S : OrdSupport β} {c d : (ρ • S : OrdSupport β)} :
-    c < d ↔ (⟨ρ⁻¹ • c.val, c.prop⟩ : S) < ⟨ρ⁻¹ • d.val, d.prop⟩ :=
-  Iff.rfl
-
-theorem lt_iff_smul' {S : OrdSupport β} {c d : S} (ρ : Allowable β) :
-    c < d ↔
-    (⟨ρ • c.val, smul_mem_smul.mpr c.prop⟩ : (ρ • S : OrdSupport β)) <
-      ⟨ρ • d.val, smul_mem_smul.mpr d.prop⟩ := by
-  simp only [lt_iff_smul, inv_smul_smul, Subtype.coe_eta]
-
-theorem lt_iff_lt_of_smul_eq {S T : OrdSupport β} (c d : T) (h : S = T)
-    (hc : c.val ∈ S) (hd : d.val ∈ S) :
-    (⟨c, hc⟩ : S) < ⟨d, hd⟩ ↔ c < d := by
-  subst h
-  rfl
-
-theorem smul_eq_of_smul_eq (ρ : Allowable β) {S : OrdSupport β} (c : S) :
-    ρ • S = S → ρ • c.val = c.val := by
-  intro hS
-  refine S.induction (motive := fun c => ρ • c.val = c.val) c ?_
-  intro c ih
-  have hc : ρ • c.val ∈ S
-  · conv_rhs => rw [← hS]
-    exact smul_mem_smul.mpr c.prop
-  have hc' : c.val ∈ ρ • S
-  · rw [hS]
-    exact c.prop
-  obtain (h | h | h) := lt_trichotomy ⟨ρ • c.val, hc⟩ c
-  · have := ih ⟨ρ • c.val, hc⟩ h
-    simp only [smul_left_cancel_iff] at this
-    exact this
-  · exact congr_arg Subtype.val h
-  · have := ih ⟨ρ⁻¹ • c.val, hc'⟩ ?_
-    · simp only [smul_inv_smul] at this
-      conv_lhs => rw [this, smul_inv_smul]
-    · rw [lt_iff_smul' ρ]
-      simp only [smul_inv_smul]
-      rw [lt_iff_lt_of_smul_eq c ⟨ρ • c.val, _⟩ hS]
-      exact h
-
-instance : MulAction (Allowable β) (OrdSupport β) where
-  one_smul S := by
-    refine ext ?_ ?_ ?_
-    · intro c hc
-      simp only [smul_mem, inv_one, one_smul] at hc
-      exact hc
-    · intro c hc
-      simp only [smul_mem, inv_one, one_smul]
-      exact hc
-    · intro c d
-      simp only [lt_iff_smul, inv_one, one_smul]
-  mul_smul ρ₁ ρ₂ S := by
-    refine ext ?_ ?_ ?_
-    · intro c hc
-      simp only [smul_mem, mul_inv_rev, mul_smul] at hc
-      exact hc
-    · intro c hc
-      simp only [smul_mem, mul_inv_rev, mul_smul]
-      exact hc
-    · intro c d
-      simp only [lt_iff_smul, mul_inv_rev, mul_smul]
-
-def relIso (S : OrdSupport β) (ρ : Allowable β) : S.r ≃r (ρ • S).r where
-  toFun c := ⟨ρ • c.val, smul_mem_smul.mpr c.prop⟩
-  invFun c := ⟨ρ⁻¹ • c.val, c.prop⟩
-  left_inv := by
-    intro c
-    simp only [coe_sort_coe, inv_smul_smul, Subtype.coe_eta]
-  right_inv := by
-    intro c
-    simp only [coe_sort_coe, smul_inv_smul, Subtype.coe_eta]
-  map_rel_iff' := by
-    intro c d
-    change _ < _ ↔ c < d
-    simp only [Equiv.coe_fn_mk, inv_smul_smul, Subtype.coe_eta]
-
-theorem relIso_apply (S : OrdSupport β) (ρ : Allowable β) (c : { c // c ∈ S.carrier }) :
-    S.relIso ρ c = ⟨ρ • c.val, smul_mem_smul.mpr c.prop⟩ :=
-  rfl
-
-@[simp]
-theorem typein_smul (S : OrdSupport β) (ρ : Allowable β) (c : (ρ • S : OrdSupport β)) :
-    Ordinal.typein (ρ • S).r c = Ordinal.typein S.r ⟨ρ⁻¹ • c.val, c.prop⟩ := by
-  have := Ordinal.relIso_enum (S.relIso ρ)
-    (Ordinal.typein S.r ⟨ρ⁻¹ • c.val, c.prop⟩) (Ordinal.typein_lt_type _ _)
-  simp only [coe_sort_coe, Ordinal.enum_typein] at this
-  have := (relIso_apply S ρ ⟨ρ⁻¹ • c.val, c.prop⟩).symm.trans this
-  have := congr_arg (Ordinal.typein (ρ • S).r) this
-  simp only [coe_sort_coe, smul_inv_smul, Subtype.coe_eta, Ordinal.typein_enum] at this
-  exact this
-
-/-- The restriction of this ordered support to conditions that come before position `i`. -/
-def before (S : OrdSupport β) (i : Ordinal.{u}) : OrdSupport β where
-  carrier := {c | ∃ hc : c ∈ S, Ordinal.typein S.r ⟨c, hc⟩ < i}
-  carrier_small := Small.mono (fun c hc => hc.1) S.small
-  r c d := (⟨c, c.prop.1⟩ : S) < ⟨d, d.prop.1⟩
-  r_isWellOrder := by
-    refine isWellOrder_invImage S.isWellOrder _ ?_
-    intro c d h
-    simp only [coe_sort_coe, mem_setOf_eq, Subtype.mk.injEq] at h
-    exact Subtype.coe_injective h
-
-@[simp]
-theorem mem_before {S : OrdSupport β} {i : Ordinal} (c : SupportCondition β) :
-    c ∈ S.before i ↔ ∃ hc : c ∈ S, Ordinal.typein S.r ⟨c, hc⟩ < i :=
-  Iff.rfl
-
-@[simp]
-theorem before_lt {S : OrdSupport β} {i : Ordinal} (c d : S.before i) :
-    c < d ↔ (⟨c, c.prop.1⟩ : S) < ⟨d, d.prop.1⟩ :=
-  Iff.rfl
-
-@[simp]
-theorem before_smul {S : OrdSupport β} {i : Ordinal} {ρ : Allowable β} :
-    (ρ • S).before i = ρ • S.before i := by
-  refine ext ?_ ?_ ?_
-  · intro c hc
-    simp only [mem_before, coe_sort_coe, OrdSupport.typein_smul, smul_mem] at hc ⊢
-    exact hc
-  · intro c hc
-    simp only [mem_before, coe_sort_coe, OrdSupport.typein_smul, smul_mem] at hc ⊢
-    exact hc
-  · intro c d
-    simp only [before_lt, lt_iff_smul]
-
-/-- Retains only those support conditions beginning with the path `A`. -/
-def comp (S : OrdSupport β) (γ : Iic α) (A : Quiver.Path (β : TypeIndex) γ) : OrdSupport γ where
-  carrier := {c | ⟨A.comp c.path, c.value⟩ ∈ S}
-  carrier_small := by
-    refine S.small.preimage ?_
-    intro c d h
-    rw [SupportCondition.mk.injEq, Quiver.Path.comp_inj_right] at h
-    exact SupportCondition.ext _ _ h.1 h.2
-  r := InvImage (· < ·) (fun c => (⟨_, c.prop⟩ : S))
-  r_isWellOrder := by
-    refine isWellOrder_invImage S.isWellOrder _ ?_
-    intro c d h
-    simp only [mem_setOf_eq, Subtype.mk.injEq, SupportCondition.mk.injEq] at h
-    rw [Quiver.Path.comp_inj_right] at h
-    exact Subtype.coe_injective (SupportCondition.ext _ _ h.1 h.2)
-
-@[simp]
-theorem mem_comp {S : OrdSupport β} (γ : Iic α) (A : Quiver.Path (β : TypeIndex) γ)
-    (c : SupportCondition γ) :
-    c ∈ S.comp γ A ↔ ⟨A.comp c.path, c.value⟩ ∈ S :=
-  Iff.rfl
-
-@[simp]
-theorem comp_lt {S : OrdSupport β} {γ : Iic α} {A : Quiver.Path (β : TypeIndex) γ}
-    {c d : S.comp γ A} :
-    c < d ↔
-    (⟨⟨A.comp c.val.path, c.val.value⟩, c.prop⟩ : S) < ⟨⟨A.comp d.val.path, d.val.value⟩, d.prop⟩ :=
-  Iff.rfl
-
-@[simp]
-theorem comp_smul {S : OrdSupport β} {γ : Iic α} {A : Quiver.Path (β : TypeIndex) γ}
-    {ρ : Allowable β} :
-    (ρ • S).comp γ A =
-    Allowable.comp (β := (β : IicBot α)) (γ := (γ : IicBot α)) A ρ • S.comp γ A := by
-  refine ext ?_ ?_ ?_
-  · intro c hc
-    simp only [mem_comp, smul_mem, Allowable.smul_supportCondition, map_inv, Tree.inv_apply] at hc ⊢
-    rw [Allowable.toStructPerm_comp (β := (β : IicBot α)) (γ := (γ : IicBot α))]
-    exact hc
-  · intro c hc
-    simp only [mem_comp, smul_mem, Allowable.smul_supportCondition, map_inv, Tree.inv_apply] at hc ⊢
-    rw [Allowable.toStructPerm_comp (β := (β : IicBot α)) (γ := (γ : IicBot α))] at hc
-    exact hc
-  · intro c d
-    simp only [comp_lt, lt_iff_smul, Allowable.smul_supportCondition, map_inv, Tree.inv_apply]
-    have := Allowable.toStructPerm_comp (β := (β : IicBot α)) (γ := (γ : IicBot α)) A
-    dsimp only at this
-    simp_rw [this]
-    simp only [Tree.comp_apply]
-
-/-- An ordered support is strong if every element of its domain is reduced, every reduced condition
-it constrains lies in its domain, and its order agrees with the constrains relation. -/
-structure Strong (S : OrdSupport β) : Prop where
-  reduced_of_mem (c : S) : Reduced c.val.value
-  transConstrains_mem (c : SupportCondition β) (d : S) : Reduced c.value → c <[α] d → c ∈ S
-  lt_of_transConstrains : (c d : S) → c.val <[α] d.val → c < d
-
-theorem Strong.fst_toNearLitter_mem {S : OrdSupport β} (hS : S.Strong)
-    {A : ExtendedIndex β} {a : Atom} (h : ⟨A, inl a⟩ ∈ S) :
-    ⟨A, inr a.1.toNearLitter⟩ ∈ S :=
-  hS.transConstrains_mem _ ⟨_, h⟩
-    (Reduced.mkLitter a.1) (Relation.TransGen.single (Constrains.atom A a))
-
-theorem Strong.before {S : OrdSupport β} (h : S.Strong) (i : Ordinal) :
-    (S.before i).Strong := by
-  constructor
-  case reduced_of_mem =>
-    intro c
-    exact h.reduced_of_mem ⟨c.val, c.prop.1⟩
-  case transConstrains_mem =>
-    intro c d hc hcd
-    refine ⟨h.transConstrains_mem c ⟨d.val, d.prop.1⟩ hc hcd, ?_⟩
-    refine lt_trans ?_ d.prop.2
-    rw [Ordinal.typein_lt_typein]
-    exact h.lt_of_transConstrains _ _ hcd
-  case lt_of_transConstrains =>
-    intro c d hcd
-    exact h.lt_of_transConstrains _ _ hcd
-
-theorem Strong.comp {S : OrdSupport β} (h : S.Strong)
-    (γ : Iic α) (A : Quiver.Path (β : TypeIndex) γ) :
-    (S.comp γ A).Strong := by
-  constructor
-  case reduced_of_mem =>
-    intro c
-    exact h.reduced_of_mem ⟨_, c.prop⟩
-  case transConstrains_mem =>
-    intro c d hc hcd
-    exact h.transConstrains_mem _ ⟨_, d.prop⟩ hc (transConstrains_comp hcd _)
-  case lt_of_transConstrains =>
-    intro c d hcd
-    exact h.lt_of_transConstrains _ _ (transConstrains_comp hcd _)
-
-/-- `T` *extends* `S` if it is a well-order that end-extends `S`. -/
-structure Extends (T S : OrdSupport β) : Prop where
-  mem_of_mem (c : S) : c.val ∈ T
-  lt_iff_lt (c d : S) :
-    c < d ↔ (⟨c, mem_of_mem c⟩ : T) < ⟨d, mem_of_mem d⟩
-  /-- If `c` is in `S ∩ T` and `d` is in `T \ S`, then `c` comes before `d`. -/
-  get_lt_get (c : S) (d : T) (hd : d.val ∉ S) :
-    ⟨c, mem_of_mem c⟩ < d
-
-instance : LE (OrdSupport β) where
-  le S T := Extends T S
-
-instance : PartialOrder (OrdSupport β) where
-  le_refl S := by
-    constructor
-    · intro c hc
-      rfl
-    · intro c d hd
-      cases hd d.prop
-  le_trans S T U hST hTU := by
-    constructor
-    · intro c d
-      rw [hST.lt_iff_lt, hTU.lt_iff_lt]
-    · intro c d hdS
-      by_cases hdT : d.val ∈ T
-      · have := hST.get_lt_get c ⟨d, hdT⟩ hdS
-        rw [hTU.lt_iff_lt] at this
-        exact this
-      · have := hTU.get_lt_get ⟨c, hST.mem_of_mem c⟩ d hdT
-        exact this
-  le_antisymm S T hST hTS := by
-    refine ext (fun c hc => hST.mem_of_mem ⟨c, hc⟩) (fun c hc => hTS.mem_of_mem ⟨c, hc⟩) ?_
-    intro c d
-    rw [hST.lt_iff_lt]
-
-theorem smul_le_smul {S T : OrdSupport β} (h : S ≤ T) (ρ : Allowable β) : ρ • S ≤ ρ • T := by
-  constructor
-  · intro c d
-    exact h.lt_iff_lt ⟨ρ⁻¹ • c.val, c.prop⟩ ⟨ρ⁻¹ • d.val, d.prop⟩
-  · intro c d
-    exact h.get_lt_get ⟨ρ⁻¹ • c.val, c.prop⟩ ⟨ρ⁻¹ • d.val, d.prop⟩
-  · intro c
-    exact h.mem_of_mem ⟨ρ⁻¹ • c.val, c.prop⟩
-
-theorem smul_le_iff_le_inv {S T : OrdSupport β} (ρ : Allowable β) : S ≤ ρ⁻¹ • T ↔ ρ • S ≤ T := by
-  constructor
-  · intro h
-    have := smul_le_smul h ρ
-    rw [smul_inv_smul] at this
-    exact this
-  · intro h
-    have := smul_le_smul h ρ⁻¹
-    rw [inv_smul_smul] at this
-    exact this
-
-theorem subset_or_subset_of_le {S₁ S₂ T : OrdSupport β}
-    (h₁ : S₁ ≤ T) (h₂ : S₂ ≤ T) :
-    (∀ c, c ∈ S₁ → c ∈ S₂) ∨ (∀ c, c ∈ S₂ → c ∈ S₁) := by
-  rw [or_iff_not_imp_left]
-  intro h c hc₂
-  by_contra hc₁
-  simp only [not_forall, exists_prop] at h
-  obtain ⟨d, hd₁, hd₂⟩ := h
-  have h₁' := h₁.get_lt_get ⟨d, hd₁⟩ ⟨c, h₂.mem_of_mem ⟨c, hc₂⟩⟩ hc₁
-  have h₂' := h₂.get_lt_get ⟨c, hc₂⟩ ⟨d, h₁.mem_of_mem ⟨d, hd₁⟩⟩ hd₂
-  exact not_lt_of_lt h₁' h₂'
-
-/-- If `ρ` maps `S` to an initial segment of itself, it is an order isomorphism. -/
-theorem lt_iff_lt_of_le {S T : OrdSupport β} {ρ : Allowable β}
-    (h₁ : ρ • S ≤ T) (h₂ : S ≤ T) (h : ∀ c, c ∈ S → ρ • c ∈ S)
-    (c d : S) :
-    c < d ↔ (⟨ρ • c.val, h c c.prop⟩ : S) < ⟨ρ • d.val, h d d.prop⟩ :=
-  by rw [lt_iff_smul' ρ, h₁.lt_iff_lt, h₂.lt_iff_lt]
-
-/-- If `ρ` maps `S` to an initial segment of itself, it is the identity function. -/
-theorem smul_eq_of_le' {S T : OrdSupport β} {ρ : Allowable β}
-    (h₁ : ρ • S ≤ T) (h₂ : S ≤ T)
-    (h : ∀ c, c ∈ S → ρ • c ∈ S)
-    (c : S) : ρ • c.val = c.val := by
-  refine S.induction (motive := fun c => ρ • c.val = c.val) c ?_
-  intro c ih
-  have hc' : c.val ∈ ρ • S
-  · by_contra hc''
-    have := h₁.get_lt_get ⟨ρ • c.val, smul_mem_smul.mpr c.prop⟩ ⟨c, h₂.mem_of_mem c⟩ hc''
-    rw [← h₂.lt_iff_lt ⟨ρ • c.val, h c c.prop⟩ c] at this
-    have h := ih ⟨ρ • c.val, h c c.prop⟩ this
-    simp only [smul_left_cancel_iff] at h
-    simp_rw [h] at this
-    exact this.false
-  obtain (hc | hc | hc) := lt_trichotomy ⟨ρ • c.val, h c c.prop⟩ c
-  · have := ih ⟨ρ • c.val, h c c.prop⟩ hc
-    simp only [smul_left_cancel_iff] at this
-    simp_rw [this] at hc
-    cases ne_of_lt hc rfl
-  · exact congr_arg Subtype.val hc
-  · have := lt_iff_lt_of_le h₁ h₂ h ⟨ρ⁻¹ • c.val, hc'⟩ c
-    simp only [smul_inv_smul, Subtype.coe_eta, hc, iff_true] at this
-    have h := ih _ this
-    simp only [smul_inv_smul] at h
-    simp_rw [← h] at this
-    cases ne_of_lt this rfl
-
-/-- `ρ` is an order isomorphism. -/
-theorem smul_eq_of_le {S T : OrdSupport β} {ρ : Allowable β}
-    (h₁ : ρ • S ≤ T) (h₂ : S ≤ T)
-    (c : S) : ρ • c.val = c.val := by
-  obtain (h | h) := subset_or_subset_of_le h₁ h₂
-  · refine smul_eq_of_le' h₁ h₂ ?_ c
-    intro c hc
-    exact h (ρ • c) (smul_mem_smul.mpr hc)
-  · have := smul_eq_of_le' (ρ := ρ⁻¹) (by rwa [inv_smul_smul]) h₁ ?_
-        ⟨ρ • c.val, smul_mem_smul.mpr c.prop⟩
-    · simp only [inv_smul_smul] at this
-      exact this.symm
-    · intro c hc
-      exact h (ρ⁻¹ • c) hc
-
-theorem eq_of_le {S T : OrdSupport β} {ρ : Allowable β}
-    (h₁ : ρ • S ≤ T) (h₂ : S ≤ T) : ρ • S = S := by
-  refine ext ?_ ?_ ?_
-  · intro c hc
-    have := smul_eq_of_le h₁ h₂ ⟨ρ⁻¹ • c, hc⟩
-    rw [smul_inv_smul] at this
-    rw [this]
-    exact hc
-  · intro c hc
-    have := smul_eq_of_le h₁ h₂ ⟨c, hc⟩
-    dsimp only at this
-    rw [smul_mem, ← this, inv_smul_smul]
-    exact hc
-  · intro c d
-    rw [h₁.lt_iff_lt, h₂.lt_iff_lt]
-
-end OrdSupport
-
-end ConNF
diff --git a/ConNF/Counting/OrdSupportExtend.lean b/ConNF/Counting/OrdSupportExtend.lean
deleted file mode 100644
index 2a94614873..0000000000
--- a/ConNF/Counting/OrdSupportExtend.lean
+++ /dev/null
@@ -1,228 +0,0 @@
-import ConNF.Counting.OrdSupport
-
-/-!
-# Extending ordered supports
--/
-
-open Set Sum
-open scoped Cardinal
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions] [FoaAssumptions α] {β : Iic α}
-
-namespace OrdSupport
-
-/-- An arbitrary global well-ordering on support conditions, such that `c ≺ d` implies `c < d`. -/
-def ConditionRel (c d : SupportCondition β) : Prop :=
-  c.value < d.value ∨ (c.value = d.value ∧ WellOrderingRel c.path d.path)
-
-theorem conditionRel_of_constrains :
-    Subrelation ((· ≺ ·) : SupportCondition β → _ → Prop) ConditionRel :=
-  Or.inl ∘ constrains_subrelation α β
-
-theorem conditionRel_of_transConstrains :
-    Subrelation ((· <[α] ·) : SupportCondition β → _ → Prop) ConditionRel :=
-  Or.inl ∘ transConstrains_subrelation β
-
-instance conditionRel_isTrichotomous : IsTrichotomous (SupportCondition β) ConditionRel := by
-  letI hlo : LinearOrder (Atom ⊕ NearLitter) := inferInstance
-  constructor
-  rintro ⟨A, x⟩ ⟨B, y⟩
-  unfold ConditionRel
-  simp only [SupportCondition.mk.injEq]
-  rw [or_iff_not_imp_left, not_or, not_and]
-  intro h₁
-  rw [or_iff_not_imp_left, not_and]
-  intro h₂
-  rw [or_iff_not_imp_left]
-  intro h₃
-  simp only [not_lt] at h₁ h₃
-  cases @le_antisymm _ hlo.toPartialOrder _ _ h₁.1 h₃
-  obtain (h | h | h) := WellOrderingRel.isWellOrder.trichotomous A B
-  · cases h₁.2 rfl h
-  · cases h₂ h rfl
-  · exact ⟨rfl, h⟩
-
-instance conditionRel_isTrans : IsTrans (SupportCondition β) ConditionRel := by
-  letI hlo : LinearOrder (Atom ⊕ NearLitter) := inferInstance
-  letI hpo : Preorder (Atom ⊕ NearLitter) := hlo.toPreorder
-  constructor
-  unfold ConditionRel
-  intro c₁ c₂ c₃ h₁ h₂
-  have := WellOrderingRel.isWellOrder.trans c₁.path c₂.path c₃.path
-  have := @lt_trans _ hlo.toPreorder c₁.value c₂.value c₃.value
-  aesop
-
-instance conditionRel_isWellFounded : IsWellFounded (SupportCondition β) ConditionRel := by
-  letI hwo : IsWellFounded (Atom ⊕ NearLitter) (· < ·) := inferInstance
-  refine ⟨⟨?_⟩⟩
-  intro c
-  refine hwo.wf.induction
-    (C := fun x => ∀ A : ExtendedIndex β, Acc ConditionRel ⟨A, x⟩) c.value ?_ c.path
-  clear c
-  intro x ih₁ A
-  refine WellOrderingRel.isWellOrder.wf.induction (C := fun A => Acc ConditionRel ⟨A, x⟩) A ?_
-  clear A
-  intro A ih₂
-  constructor
-  rintro c (hc | ⟨rfl, hc⟩)
-  · exact ih₁ c.value hc c.path
-  · exact ih₂ c.path hc
-
-instance : IsWellOrder (SupportCondition β) ConditionRel := ⟨⟩
-
-/-- Extends the well-order `S` to a well-order of `SupportCondition β`, in such a way that `S`
-is an initial segment. -/
-@[mk_iff]
-inductive ExtendRel (S : OrdSupport β) : SupportCondition β → SupportCondition β → Prop
-| lt (c d : S) : c < d → ExtendRel S c d
-| conditionRel (c d : SupportCondition β) : c ∉ S → d ∉ S → ConditionRel c d → ExtendRel S c d
-| sep (c : S) (d : SupportCondition β) : d ∉ S → ExtendRel S c d
-
-instance (S : OrdSupport β) : IsTrichotomous (SupportCondition β) (ExtendRel S) := by
-  constructor
-  intro c d
-  by_cases hc : c ∈ S <;> by_cases hd : d ∈ S
-  · obtain (h | h | h) := lt_trichotomy (⟨c, hc⟩ : S) ⟨d, hd⟩
-    · exact Or.inl (ExtendRel.lt ⟨c, hc⟩ ⟨d, hd⟩ h)
-    · rw [Subtype.mk.injEq] at h
-      exact Or.inr (Or.inl h)
-    · exact Or.inr (Or.inr (ExtendRel.lt ⟨d, hd⟩ ⟨c, hc⟩ h))
-  · exact Or.inl (ExtendRel.sep ⟨c, hc⟩ d hd)
-  · exact Or.inr (Or.inr (ExtendRel.sep ⟨d, hd⟩ c hc))
-  · obtain (h | h | h) := conditionRel_isTrichotomous.trichotomous c d
-    · exact Or.inl (ExtendRel.conditionRel c d hc hd h)
-    · exact Or.inr (Or.inl h)
-    · exact Or.inr (Or.inr (ExtendRel.conditionRel d c hd hc h))
-
-instance (S : OrdSupport β) : IsTrans (SupportCondition β) (ExtendRel S) := by
-  constructor
-  intro c₁ c₂ c₃ h₁ h₂
-  cases h₁ with
-  | lt c₁ c₂ h₁ =>
-    obtain ⟨c₂, hc₂⟩ := c₂
-    cases h₂ with
-    | lt c₂ c₃ h₂ =>
-      exact ExtendRel.lt c₁ c₃ (h₁.trans h₂)
-    | conditionRel c₂ c₃ hc₂' hc₃ h₂ =>
-      cases hc₂' hc₂
-    | sep c₂ c₃ hc₃ =>
-      exact ExtendRel.sep c₁ c₃ hc₃
-  | conditionRel c₁ c₂ hc₁ hc₂ h₁ =>
-    cases h₂ with
-    | lt c₂ c₃ h₂ =>
-      cases hc₂ c₂.prop
-    | conditionRel c₂ c₃ hc₂' hc₃ h₂ =>
-      exact ExtendRel.conditionRel c₁ c₃ hc₁ hc₃ (conditionRel_isTrans.trans c₁ c₂ c₃ h₁ h₂)
-    | sep c₂ c₃ hc₃ =>
-      cases hc₂ c₂.prop
-  | sep c₁ c₂ hc₂ =>
-    cases h₂ with
-    | lt c₂ c₃ h₂ =>
-      cases hc₂ c₂.prop
-    | conditionRel c₂ c₃ hc₂' hc₃ h₂ =>
-      exact ExtendRel.sep c₁ c₃ hc₃
-    | sep c₂ c₃ hc₃ =>
-      cases hc₂ c₂.prop
-
-theorem mem_of_extendRel {S : OrdSupport β} (c : SupportCondition β) (d : S)
-    (h : ExtendRel S c d) : c ∈ S := by
-  obtain ⟨d, hd⟩ := d
-  cases h with
-  | lt c d h =>
-    exact c.prop
-  | conditionRel c d hc hd' h =>
-    cases hd' hd
-  | sep c d h =>
-    cases h hd
-
-theorem lt_of_extendRel {S : OrdSupport β} (c : SupportCondition β) (d : S)
-    (h : ExtendRel S c d) : ⟨c, mem_of_extendRel c d h⟩ < d := by
-  obtain ⟨d, hd⟩ := d
-  cases h with
-  | lt c d h =>
-    exact h
-  | conditionRel c d hc hd' h =>
-    cases hd' hd
-  | sep c d h =>
-    cases h hd
-
-instance (S : OrdSupport β) : IsWellFounded (SupportCondition β) (ExtendRel S) := by
-  constructor
-  have : ∀ c : S, Acc (ExtendRel S) c
-  · intro c
-    refine S.induction (motive := fun c => Acc (ExtendRel S) c) c ?_
-    intro c ih
-    constructor
-    intro d hd
-    exact ih ⟨d, mem_of_extendRel d c hd⟩ (lt_of_extendRel d c hd)
-  constructor
-  intro c
-  refine conditionRel_isWellFounded.induction (C := fun c => Acc (ExtendRel S) c) c ?_
-  intro c ih
-  constructor
-  intro d hd
-  cases hd with
-  | lt c d h =>
-    exact this c
-  | conditionRel c d hc hd' h =>
-    exact ih d h
-  | sep c d h =>
-    exact this c
-
-instance (S : OrdSupport β) : IsWellOrder (SupportCondition β) (ExtendRel S) := ⟨⟩
-
-/-- Add some extra support conditions to the end of an ordered support. -/
-noncomputable def extend (S : OrdSupport β) (s : Set (SupportCondition β)) (hs : Small s) :
-    OrdSupport β where
-  carrier := S ∪ s
-  carrier_small := Small.union S.small hs
-  r c d := ExtendRel S c d
-  r_isWellOrder := isWellOrder_invImage
-    (inferInstanceAs (IsWellOrder (SupportCondition β) (ExtendRel S))) _ Subtype.val_injective
-
-/-- An extended support specialises the original. -/
-theorem le_extend (S : OrdSupport β) (s : Set (SupportCondition β)) (hs : Small s) :
-    S ≤ S.extend s hs where
-  mem_of_mem c := Or.inl c.prop
-  lt_iff_lt c d := ⟨ExtendRel.lt c d, fun h => lt_of_extendRel c d (show ExtendRel S c d from h)⟩
-  get_lt_get c d hd := ExtendRel.sep c d hd
-
-theorem mem_extend_iff (S : OrdSupport β) (s : Set (SupportCondition β)) (hs : Small s)
-    (c : SupportCondition β) :
-    c ∈ S.extend s hs ↔ c ∈ S ∨ c ∈ s :=
-  Iff.rfl
-
-theorem extend_strong {S : OrdSupport β} {s : Set (SupportCondition β)} {hs : Small s}
-    (hS : S.Strong) (hs₁ : ∀ c ∈ s, Reduced c.value)
-    (hs₂ : ∀ c ∈ s, ∀ d : SupportCondition β, Reduced d.value → d <[α] c → d ∈ s) :
-    (S.extend s hs).Strong := by
-  constructor
-  case reduced_of_mem =>
-    intro c
-    obtain (hc | hc) := c.prop
-    · exact hS.reduced_of_mem ⟨c, hc⟩
-    · exact hs₁ c hc
-  case transConstrains_mem =>
-    intro c d hc hcd
-    obtain (hd | hd) := d.prop
-    · exact Or.inl (hS.transConstrains_mem c ⟨d, hd⟩ hc hcd)
-    · exact Or.inr (hs₂ d hd c hc hcd)
-  case lt_of_transConstrains =>
-    intro c d hcd
-    by_cases hd : d.val ∈ S
-    · refine ExtendRel.lt ⟨c.val, ?_⟩ ⟨d.val, hd⟩ ?_
-      · by_contra hcS
-        have hcs := or_iff_not_imp_left.mp c.prop hcS
-        exact hcS (hS.transConstrains_mem c ⟨d.val, hd⟩ (hs₁ c hcs) hcd)
-      · exact hS.lt_of_transConstrains _ _ hcd
-    by_cases hc : c.val ∈ S
-    · exact ExtendRel.sep ⟨c.val, hc⟩ d hd
-    · exact ExtendRel.conditionRel c.val d.val hc hd (conditionRel_of_transConstrains hcd)
-
-end OrdSupport
-
-end ConNF
diff --git a/ConNF/Counting/OrdSupportOrbit.lean b/ConNF/Counting/OrdSupportOrbit.lean
deleted file mode 100644
index c802c22b2b..0000000000
--- a/ConNF/Counting/OrdSupportOrbit.lean
+++ /dev/null
@@ -1,100 +0,0 @@
-import Mathlib.GroupTheory.GroupAction.Basic
-import ConNF.Counting.OrdSupport
-
-/-!
-# Orbits of ordered supports
--/
-
-open Set MulAction
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions] [FoaAssumptions α] {β : Iic α}
-
-def OrdSupportOrbit (β : Iic α) : Type u :=
-  orbitRel.Quotient (Allowable β) (OrdSupport β)
-
-namespace OrdSupportOrbit
-
-/-- The orbit of a given ordered support. -/
-def mk (S : OrdSupport β) : OrdSupportOrbit β :=
-  ⟦S⟧
-
-protected theorem eq {S T : OrdSupport β} : mk S = mk T ↔ S ∈ orbit (Allowable β) T :=
-  Quotient.eq (r := _)
-
-instance : SetLike (OrdSupportOrbit β) (OrdSupport β) where
-  coe o := {S | mk S = o}
-  coe_injective' := by
-    intro o₁ o₂
-    refine Quotient.inductionOn₂ o₁ o₂ ?_
-    intro S₁ S₂ h
-    simp only [ext_iff, mem_setOf_eq] at h
-    exact (h S₁).mp rfl
-
-theorem mem_mk (S : OrdSupport β) : S ∈ mk S :=
-  rfl
-
-theorem mem_def (S : OrdSupport β) (o : OrdSupportOrbit β) : S ∈ o ↔ mk S = o := Iff.rfl
-
-@[simp]
-theorem mem_mk_iff (S T : OrdSupport β) : S ∈ mk T ↔ S ∈ orbit (Allowable β) T := by
-  rw [mem_def, mk, mk, ← orbitRel_apply, Quotient.eq (r := _)]
-  rfl
-
-theorem smul_mem_of_mem {S : OrdSupport β} {o : OrdSupportOrbit β} (ρ : Allowable β) (h : S ∈ o) :
-    ρ • S ∈ o := by
-  refine Quotient.inductionOn o ?_ h
-  intro T hST
-  change _ ∈ mk _ at hST ⊢
-  rw [mem_mk_iff] at hST ⊢
-  obtain ⟨ρ', rfl⟩ := hST
-  rw [smul_smul]
-  exact ⟨ρ * ρ', rfl⟩
-
-theorem smul_mem_iff_mem {S : OrdSupport β} {o : OrdSupportOrbit β} (ρ : Allowable β) :
-    ρ • S ∈ o ↔ S ∈ o := by
-  refine ⟨?_, smul_mem_of_mem ρ⟩
-  intro h
-  have := smul_mem_of_mem ρ⁻¹ h
-  rw [inv_smul_smul] at this
-  exact this
-
-theorem eq_of_mem_orbit {o₁ o₂ : OrdSupportOrbit β} {S₁ S₂ : OrdSupport β}
-    (h₁ : S₁ ∈ o₁) (h₂ : S₂ ∈ o₂) (h : S₁ ∈ orbit (Allowable β) S₂) : o₁ = o₂ := by
-  rw [mem_def] at h₁ h₂
-  rw [← h₁, ← h₂, OrdSupportOrbit.eq]
-  exact h
-
-noncomputable def out (o : OrdSupportOrbit β) : OrdSupport β :=
-  Quotient.out (s := _) o
-
-theorem out_mem (o : OrdSupportOrbit β) : o.out ∈ o :=
-  Quotient.out_eq (s := _) o
-
-theorem nonempty (o : OrdSupportOrbit β) : (o : Set (OrdSupport β)).Nonempty :=
-  ⟨o.out, o.out_mem⟩
-
-theorem eq_mk_of_mem {S : OrdSupport β} {o : OrdSupportOrbit β} (h : S ∈ o) : o = mk S :=
-  h.symm
-
-/-- An orbit of ordered supports is *strong* if it contains a strong support. -/
-def Strong (o : OrdSupportOrbit β) : Prop :=
-  ∃ S : OrdSupport β, o = mk S ∧ S.Strong
-
-/-- A strong support in this strong orbit. -/
-noncomputable def Strong.out {o : OrdSupportOrbit β} (h : o.Strong) : OrdSupport β :=
-  h.choose
-
-@[simp]
-theorem Strong.mk_out {o : OrdSupportOrbit β} (h : o.Strong) : mk h.out = o :=
-  h.choose_spec.1.symm
-
-theorem Strong.out_strong {o : OrdSupportOrbit β} (h : o.Strong) : h.out.Strong :=
-  h.choose_spec.2
-
-end OrdSupportOrbit
-
-end ConNF
diff --git a/ConNF/Counting/OrdSupportOrbitEquiv.lean b/ConNF/Counting/OrdSupportOrbitEquiv.lean
deleted file mode 100644
index cf05b764b5..0000000000
--- a/ConNF/Counting/OrdSupportOrbitEquiv.lean
+++ /dev/null
@@ -1,185 +0,0 @@
-import ConNF.Counting.OrdSupportOrbit
-import ConNF.Counting.SpecSame
-
-open Set
-open scoped Cardinal
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions] [FoaAssumptions α] {β : Iic α}
-
-noncomputable def InflexibleCoe.smul {A : ExtendedIndex β} {L : Litter}
-    (h : InflexibleCoe A L) (ρ : Allowable β) :
-    InflexibleCoe A (Allowable.toStructPerm ρ A • L) where
-  path := h.path
-  t := Allowable.comp (show Quiver.Path ((β : IicBot α) : TypeIndex) (h.path.δ : IicBot α) from
-    h.path.B.cons (WithBot.coe_lt_coe.mpr h.path.hδ)) ρ • h.t
-  hL := by
-    have := toStructPerm_smul_fuzz (β : IicBot α) h.path.γ h.path.δ h.path.ε ?_ ?_ ?_
-      h.path.B ρ h.t
-    rw [← this, ← h.path.hA, ← h.hL]
-    · intro hδε
-      simp only [Subtype.mk.injEq, WithBot.coe_inj] at hδε
-      exact h.path.hδε (Subtype.coe_injective hδε)
-    · exact WithBot.coe_lt_coe.mpr h.path.hε
-    · exact WithBot.coe_lt_coe.mpr h.path.hδ
-
-@[simp]
-theorem InflexibleCoe.smul_path {A : ExtendedIndex β} {L : Litter}
-    (h : InflexibleCoe A L) (ρ : Allowable β) :
-    (h.smul ρ).path = h.path :=
-  rfl
-
-@[simp]
-theorem InflexibleCoe.smul_t {A : ExtendedIndex β} {L : Litter}
-    (h : InflexibleCoe A L) (ρ : Allowable β) :
-    (h.smul ρ).t =
-    Allowable.comp (show Quiver.Path ((β : IicBot α) : TypeIndex) (h.path.δ : IicBot α) from
-      h.path.B.cons (WithBot.coe_lt_coe.mpr h.path.hδ)) ρ • h.t :=
-  rfl
-
-noncomputable def InflexibleBot.smul {A : ExtendedIndex β} {L : Litter}
-    (h : InflexibleBot A L) (ρ : Allowable β) :
-    InflexibleBot A (Allowable.toStructPerm ρ A • L) where
-  path := h.path
-  a := Allowable.toStructPerm ρ (h.path.B.cons (WithBot.bot_lt_coe _)) • h.a
-  hL := by
-    refine Eq.trans ?_ (congr_arg _
-      (comp_bot_smul_atom (β := (β : IicBot α)) ρ (Quiver.Path.cons h.path.B ?_) h.a))
-    refine Eq.trans ?_ (toStructPerm_smul_fuzz (β : IicBot α) h.path.γ ⊥ h.path.ε ?_ ?_ ?_
-      h.path.B ρ h.a)
-    rw [← h.path.hA, ← h.hL]
-    · intro hδε
-      simp only [IioBot.bot_ne_mk_coe] at hδε
-    · exact WithBot.coe_lt_coe.mpr h.path.hε
-    · exact WithBot.bot_lt_coe _
-    · exact WithBot.bot_lt_coe _
-
-@[simp]
-theorem InflexibleBot.smul_path {A : ExtendedIndex β} {L : Litter}
-    (h : InflexibleBot A L) (ρ : Allowable β) :
-    (h.smul ρ).path = h.path :=
-  rfl
-
-@[simp]
-theorem InflexibleBot.smul_a {A : ExtendedIndex β} {L : Litter}
-    (h : InflexibleBot A L) (ρ : Allowable β) :
-    (h.smul ρ).a = Allowable.toStructPerm ρ (h.path.B.cons (WithBot.bot_lt_coe _)) • h.a :=
-  rfl
-
-theorem Flexible.smul {A : ExtendedIndex β} {L : Litter}
-    (h : Flexible α A L) (ρ : Allowable β) :
-    Flexible α A (Allowable.toStructPerm ρ A • L) := by
-  obtain (hL | ⟨⟨hL⟩⟩ | ⟨⟨hL⟩⟩) := flexible_cases' β A (Allowable.toStructPerm ρ A • L)
-  · exact hL
-  · have := hL.smul ρ⁻¹
-    simp only [map_inv, Tree.inv_apply, inv_smul_smul] at this
-    cases h (inflexible_of_inflexibleBot this)
-  · have := hL.smul ρ⁻¹
-    simp only [map_inv, Tree.inv_apply, inv_smul_smul] at this
-    cases h (inflexible_of_inflexibleCoe this)
-
-def Spec.specifies_smul (σ : Spec β) (S : OrdSupport β) (hσS : Specifies σ S) (ρ : Allowable β) :
-    σ.Specifies (ρ • S) := by
-  constructor
-  case lt_orderType =>
-    intro c
-    rw [OrdSupport.typein_smul]
-    exact hσS.lt_orderType _
-  case of_lt_orderType =>
-    intro i hi
-    obtain ⟨c, hc⟩ := hσS.of_lt_orderType i hi
-    refine ⟨⟨ρ • c.val, OrdSupport.smul_mem_smul.mpr c.prop⟩, ?_⟩
-    simp only [OrdSupport.coe_sort_coe, OrdSupport.typein_smul, inv_smul_smul, Subtype.coe_eta]
-    exact hc
-  case atom_dom =>
-    intro A a h
-    simp only [OrdSupport.smul_mem, Allowable.smul_supportCondition, map_inv, Tree.inv_apply,
-      Sum.smul_inl] at h
-    obtain ⟨N, hN₁, hN₂⟩ := hσS.atom_dom A ((Allowable.toStructPerm ρ A)⁻¹ • a) h
-    refine ⟨Allowable.toStructPerm ρ A • N, hN₁, ?_⟩
-    have := (OrdSupport.smul_mem_smul (ρ := ρ)).mpr hN₂
-    simp only [Allowable.smul_supportCondition, Sum.smul_inr] at this
-    exact this
-  case atom_spec =>
-    intro A a N ha hN haN
-    simp only [OrdSupport.coe_sort_coe, OrdSupport.typein_smul]
-    simp only [OrdSupport.coe_sort_coe, Allowable.smul_supportCondition, map_inv, Tree.inv_apply,
-      Sum.smul_inl, Sum.smul_inr]
-    refine hσS.atom_spec A ((Allowable.toStructPerm ρ A)⁻¹ • a)
-      ((Allowable.toStructPerm ρ A)⁻¹ • N) _ _ ?_
-    change (Allowable.toStructPerm ρ A) • (Allowable.toStructPerm ρ A)⁻¹ • a ∈ N
-    rw [smul_inv_smul]
-    exact haN
-  case flexible_spec =>
-    intro A N hNS hN
-    simp only [OrdSupport.coe_sort_coe, OrdSupport.typein_smul]
-    exact hσS.flexible_spec A (Allowable.toStructPerm ρ⁻¹ A • N) hNS (hN.smul ρ⁻¹)
-  case inflexibleCoe_spec =>
-    rintro A N hNS hN
-    obtain ⟨χ, hχ₁, hχ₂, h₁, h₂⟩ := hσS.inflexibleCoe_spec A
-      (Allowable.toStructPerm ρ⁻¹ A • N) hNS (hN.smul ρ⁻¹)
-    refine ⟨χ, hχ₁, ?_, ?_, ?_⟩
-    · simp only [OrdSupport.coe_sort_coe, OrdSupport.typein_smul, OrdSupport.before_smul,
-        OrdSupport.comp_smul]
-      exact χ.smul_mem _ hχ₂
-    · simp only [OrdSupport.coe_sort_coe, OrdSupport.typein_smul, OrdSupport.before_smul,
-        OrdSupport.comp_smul]
-      simp only [NearLitterPerm.smul_nearLitter_fst, InflexibleCoe.smul_path,
-        OrdSupport.coe_sort_coe, map_inv, Tree.inv_apply, InflexibleCoe.smul_t] at h₁
-      rw [eq_inv_smul_iff] at h₁
-      rw [χ.decode_smul, ← h₁]
-      simp only [NearLitterPerm.smul_nearLitter_fst, InflexibleCoe.smul_path,
-        OrdSupport.coe_sort_coe, Allowable.smul_supportCondition, map_inv, Tree.inv_apply,
-        Sum.smul_inr]
-    · simp only [OrdSupport.coe_sort_coe, OrdSupport.typein_smul, Allowable.smul_supportCondition,
-        map_inv, Tree.inv_apply, Sum.smul_inr]
-      simp only [OrdSupport.coe_sort_coe, map_inv, Tree.inv_apply, NearLitterPerm.smul_nearLitter_fst,
-        InflexibleCoe.smul_path] at h₂
-      exact h₂
-  case inflexibleBot_spec =>
-    intro A N hNS hN
-    obtain ⟨h₁, h₂⟩ := hσS.inflexibleBot_spec A (Allowable.toStructPerm ρ⁻¹ A • N) hNS (hN.smul ρ⁻¹)
-    refine ⟨h₁, ?_⟩
-    simp only [OrdSupport.coe_sort_coe, OrdSupport.typein_smul, Allowable.smul_supportCondition,
-      map_inv, Tree.inv_apply, Sum.smul_inr, Sum.smul_inl]
-    simp only [OrdSupport.coe_sort_coe, map_inv, Tree.inv_apply, NearLitterPerm.smul_nearLitter_fst,
-      InflexibleBot.smul_path, InflexibleBot.smul_a] at h₂
-    exact h₂
-
-/-- There is an equivalence between strong ordered support orbits and strong specifications. -/
-noncomputable def specEquiv (β : Iic α) :
-    { o : OrdSupportOrbit β // o.Strong } ≃ { σ : Spec β // σ.Strong } where
-  toFun o := ⟨Spec.spec o.prop.out o.prop.out_strong,
-    o.prop.out, o.prop.out_strong, Spec.spec_specifies _⟩
-  invFun σ := ⟨OrdSupportOrbit.mk σ.prop.out, σ.prop.out, rfl, σ.prop.out_strong⟩
-  left_inv := by
-    intro o
-    refine Subtype.coe_injective ?_
-    dsimp only
-    conv_rhs => rw [← o.prop.mk_out]
-    rw [OrdSupportOrbit.eq]
-    have h₁ := Spec.spec_specifies o.prop.out_strong
-    have h₂ := Spec.Strong.specifies_out (σ := Spec.spec o.prop.out o.prop.out_strong)
-      ⟨o.prop.out, o.prop.out_strong, Spec.spec_specifies _⟩
-    exact ⟨_, Spec.convertAllowable_smul h₁ h₂ o.prop.out_strong (Spec.Strong.out_strong _)⟩
-  right_inv := by
-    intro σ
-    refine Subtype.coe_injective ?_
-    have := OrdSupportOrbit.Strong.mk_out ⟨σ.prop.out, rfl, σ.prop.out_strong⟩
-    rw [OrdSupportOrbit.eq] at this
-    obtain ⟨ρ, h⟩ := this
-    simp_rw [← h]
-    have h₁ := σ.prop.specifies_out
-    have := Spec.specifies_smul σ.val _ h₁ ρ
-    exact Spec.specifies_subsingleton _ (Spec.spec_specifies _) this
-
-/-- The amount of strong support orbits is exactly the amount of strong specifications. -/
-noncomputable def mk_ordSupportOrbit (β : Iic α) :
-    Cardinal.lift.{u + 1} #{ o : OrdSupportOrbit β // o.Strong } = #{ σ : Spec β // σ.Strong } := by
-  rw [Cardinal.lift_mk_eq'.mpr ⟨specEquiv β⟩]
-  exact Cardinal.lift_id'.{u, u + 1} _
-
-end ConNF
diff --git a/ConNF/Counting/Recode.lean b/ConNF/Counting/Recode.lean
deleted file mode 100644
index 442030e5c6..0000000000
--- a/ConNF/Counting/Recode.lean
+++ /dev/null
@@ -1,332 +0,0 @@
-import ConNF.Structural.Pretangle
-import ConNF.Counting.Hypotheses
-import ConNF.Counting.OrdSupportExtend
-import ConNF.Counting.OrdSupportOrbit
-import ConNF.Counting.CodingFunction
-
-/-!
-# Raising supports to higher levels
--/
-
-open MulAction Quiver Set Sum WithBot
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions] [CountingAssumptions α] {β γ : Iic α} (hγ : γ < β)
-
-def raiseIndex (A : ExtendedIndex (γ : TypeIndex)) : ExtendedIndex β :=
-  (Hom.toPath hγ).comp A
-
-def raise (c : SupportCondition γ) : SupportCondition β :=
-  ⟨raiseIndex hγ c.path, c.value⟩
-
-@[simp]
-theorem raise_path (c : SupportCondition γ) : (raise hγ c).path = raiseIndex hγ c.path := rfl
-
-@[simp]
-theorem raise_value (c : SupportCondition γ) : (raise hγ c).value = c.value := rfl
-
-theorem smul_raise_eq_iff (c : SupportCondition γ) (ρ : Allowable β) :
-    ρ • raise hγ c = raise hγ c ↔
-    Allowable.comp (Hom.toPath
-      (show (γ : IicBot α) < β from coe_lt_coe.mpr hγ)) ρ • c = c := by
-  obtain ⟨A, x⟩ := c
-  rw [raise, Allowable.smul_supportCondition, Allowable.smul_supportCondition]
-  simp only [raise_path, raise_value, SupportCondition.mk.injEq, true_and]
-  rw [Allowable.toStructPerm_comp (Hom.toPath
-      (show (γ : IicBot α) < β from coe_lt_coe.mpr hγ)),
-    Tree.comp_apply,
-    raiseIndex]
-
-/-- A set `s` of `γ`-pretangles *appears* at level `α` if it occurs as the `γ`-extension of some
-`α`-tangle. -/
-def Appears (s : Set (Pretangle γ)) : Prop :=
-  ∃ t : Tangle β,
-    s = Pretangle.ofCoe (toPretangle (β : IicBot α) t) γ (coe_lt_coe.mpr hγ)
-
-/-- Convert a set of `γ`-tangles to the (unique) `α`-tangle with that `γ`-extension,
-if it exists. -/
-noncomputable def toTangle (s : Set (Pretangle γ)) (h : Appears hγ s) : Tangle β :=
-  h.choose
-
-theorem toPretangle_toTangle (s : Set (Pretangle γ)) (h : Appears hγ s) :
-    s = Pretangle.ofCoe (toPretangle (β : IicBot α) (toTangle hγ s h)) γ (coe_lt_coe.mpr hγ) :=
-  h.choose_spec
-
-def AppearsRaised
-    (χs : Set (CodingFunction β)) (U : OrdSupport β) : Prop :=
-  Appears hγ {u | ∃ χ ∈ χs, ∃ V ≥ U, ∃ hV : V ∈ χ,
-    u ∈ Pretangle.ofCoe (toPretangle (β : IicBot α) ((χ.decode V).get hV)) γ (coe_lt_coe.mpr hγ)}
-
-noncomputable def decodeRaised (χs : Set (CodingFunction β))
-    (U : OrdSupport β) (hU : AppearsRaised hγ χs U) : Tangle β :=
-  hU.choose
-
-/-!
-We now aim to show that `decodeRaised` is a coding function.
--/
-
-theorem decodeRaised_spec (χs : Set (CodingFunction β))
-    (U : OrdSupport β) (hU : AppearsRaised hγ χs U) :
-    Pretangle.ofCoe (toPretangle (β : IicBot α) (decodeRaised hγ χs U hU))
-      γ (coe_lt_coe.mpr hγ) =
-    {u | ∃ χ ∈ χs, ∃ V ≥ U, ∃ hV : V ∈ χ,
-      u ∈ Pretangle.ofCoe (toPretangle (β : IicBot α) ((χ.decode V).get hV))
-        γ (coe_lt_coe.mpr hγ)} :=
-  hU.choose_spec.symm
-
-theorem appearsRaised_smul {χs : Set (CodingFunction β)}
-    (U : OrdSupport β) (hU : AppearsRaised hγ χs U) (ρ : Allowable β) :
-    AppearsRaised hγ χs (ρ • U) := by
-  obtain ⟨t, ht⟩ := hU
-  refine ⟨ρ • t, ?_⟩
-  rw [toPretangle_smul, Allowable.toStructPerm_smul, StructPerm.ofCoe_smul, ← ht]
-  ext u
-  constructor
-  · simp only [ge_iff_le, mem_setOf_eq, forall_exists_index, and_imp]
-    intro χ hχ V hUV hVχ hu
-    refine ⟨(Tree.comp (Hom.toPath (coe_lt_coe.mpr hγ)) (Allowable.toStructPerm ρ))⁻¹ • u,
-      ?_, by simp only [smul_inv_smul]⟩
-    refine ⟨χ, hχ, ρ⁻¹ • V, by rwa [OrdSupport.smul_le_iff_le_inv],
-      CodingFunction.smul_mem _ hVχ, ?_⟩
-    rw [CodingFunction.decode_smul, toPretangle_smul, Allowable.toStructPerm_smul,
-      StructPerm.ofCoe_smul, map_inv, Tree.comp_inv, smul_mem_smul_set_iff]
-    exact hu
-  · simp only [ge_iff_le, mem_setOf_eq]
-    rintro ⟨u, ⟨χ, hχ, V, hUV, hVχ, hu⟩, rfl⟩
-    refine ⟨χ, hχ, ρ • V, OrdSupport.smul_le_smul hUV ρ, CodingFunction.smul_mem _ hVχ, ?_⟩
-    rw [CodingFunction.decode_smul, toPretangle_smul, Allowable.toStructPerm_smul,
-      StructPerm.ofCoe_smul, smul_mem_smul_set_iff]
-    exact hu
-
-theorem decodeRaised_smul {χs : Set (CodingFunction β)}
-    (U : OrdSupport β) (hU : AppearsRaised hγ χs U) (ρ : Allowable β) :
-    decodeRaised hγ χs (ρ • U) (appearsRaised_smul hγ U hU ρ) = ρ • decodeRaised hγ χs U hU := by
-  refine CountingAssumptions.toPretangle_ext β γ hγ _ _ ?_
-  intro u
-  rw [toPretangle_smul, Allowable.toStructPerm_smul, StructPerm.ofCoe_smul,
-    decodeRaised_spec, decodeRaised_spec]
-  -- TODO: Unify this proof with the previous by extracting a lemma.
-  constructor
-  · simp only [ge_iff_le, mem_setOf_eq, forall_exists_index, and_imp]
-    intro χ hχ V hUV hVχ hu
-    refine ⟨(Tree.comp (Hom.toPath (coe_lt_coe.mpr hγ)) (Allowable.toStructPerm ρ))⁻¹ • u,
-      ?_, by simp only [smul_inv_smul]⟩
-    refine ⟨χ, hχ, ρ⁻¹ • V, by rwa [OrdSupport.smul_le_iff_le_inv],
-      CodingFunction.smul_mem _ hVχ, ?_⟩
-    rw [CodingFunction.decode_smul, toPretangle_smul, Allowable.toStructPerm_smul,
-      StructPerm.ofCoe_smul, map_inv, Tree.comp_inv, smul_mem_smul_set_iff]
-    exact hu
-  · simp only [ge_iff_le, mem_setOf_eq]
-    rintro ⟨u, ⟨χ, hχ, V, hUV, hVχ, hu⟩, rfl⟩
-    refine ⟨χ, hχ, ρ • V, OrdSupport.smul_le_smul hUV ρ, CodingFunction.smul_mem _ hVχ, ?_⟩
-    rw [CodingFunction.decode_smul, toPretangle_smul, Allowable.toStructPerm_smul,
-      StructPerm.ofCoe_smul, smul_mem_smul_set_iff]
-    exact hu
-
-/-- The tangles in the `γ`-extension of a given `α`-tangle. -/
-def tangleExtension (t : Tangle β) : Set (Tangle γ) :=
-  {u | toPretangle (γ : IicBot α) u ∈
-    Pretangle.ofCoe (toPretangle (β : IicBot α) t) γ (coe_lt_coe.mpr hγ)}
-
-/-- A support for a `γ`-tangle, expressed as a set of `α`-support conditions. -/
-noncomputable def raisedSupport (S : OrdSupport β) (u : Tangle γ) :
-    OrdSupport β :=
-  S.extend
-    (reduction α (raise hγ '' (reducedSupport α u).carrier))
-    (reduction_small _ (Small.image (reduction_small α (designatedSupport u).small)))
-
-theorem raisedSupport_strong (S : OrdSupport β) (hS : S.Strong) (u : Tangle γ) :
-    (raisedSupport hγ S u).Strong := by
-  refine OrdSupport.extend_strong hS ?_ ?_
-  · intro c hc
-    exact hc.2
-  · rintro c ⟨⟨e, he₁, he₂⟩, _⟩ d hd hcd
-    refine ⟨?_, hd⟩
-    exact ⟨e, he₁, hcd.to_reflTransGen.trans he₂⟩
-
-theorem raisedSupport_supports (S : OrdSupport β) (u : Tangle γ) :
-    Supports (Allowable β) {c | c ∈ raisedSupport hγ S u}
-      (singleton β γ (coe_lt_coe.mpr hγ) u) := by
-  intro ρ h
-  rw [singleton_smul β γ]
-  refine congr_arg _ ?_
-  refine (reducedSupport α u).supports _ ?_
-  intro c hc
-  rw [← smul_raise_eq_iff]
-  refine h ?_
-  rw [mem_setOf, raisedSupport, OrdSupport.mem_extend_iff]
-  refine Or.inr ⟨?_, hc.2⟩
-  exact mem_reflTransClosure_of_mem α _ _ ⟨_, hc, rfl⟩
-
-theorem le_raisedSupport (S : OrdSupport β) (u : Tangle γ) :
-    S ≤ raisedSupport hγ S u :=
-  OrdSupport.le_extend _ _ _
-
-noncomputable def raiseSingleton (S : OrdSupport β) (u : Tangle γ) : CodingFunction β :=
-  CodingFunction.code
-    (raisedSupport hγ S u)
-    (singleton β γ (coe_lt_coe.mpr hγ) u)
-    (raisedSupport_supports hγ S u)
-
-def RaisedSingleton : Type u :=
-  {χ : CodingFunction β // ∃ S : OrdSupport β, ∃ u : Tangle γ, χ = raiseSingleton hγ S u}
-
-/-- Take the `γ`-extension of `t`, treated as a set of `α`-level singletons, and turn them into
-coding functions. -/
-def raiseSingletons (S : OrdSupport β) (t : Tangle β) : Set (CodingFunction β) :=
-  raiseSingleton hγ S '' tangleExtension hγ t
-
-theorem raiseSingletons_subset_range {S : OrdSupport β} {t : Tangle β} :
-    raiseSingletons hγ S t ⊆
-    range (Subtype.val : RaisedSingleton hγ → CodingFunction β) := by
-  rintro _ ⟨u, _, rfl⟩
-  exact ⟨⟨raiseSingleton hγ S u, ⟨S, u, rfl⟩⟩, rfl⟩
-
-theorem smul_reducedSupport_eq (S : OrdSupport β) (v : Tangle γ) (ρ : Allowable β)
-    (hUV : S ≤ ρ • raisedSupport hγ S v)
-    (c : SupportCondition β) (hc : c ∈ S) : ρ • c = c := by
-  have := OrdSupport.eq_of_le (OrdSupport.smul_le_smul (le_raisedSupport hγ S v) ρ) hUV
-  exact OrdSupport.smul_eq_of_smul_eq ρ ⟨c, hc⟩ this
-
-theorem raiseSingletons_reducedSupport (S : OrdSupport β) (t : Tangle β)
-    (hSt : Supports (Allowable β) {c | c ∈ S} t) :
-    {u | ∃ χ ∈ raiseSingletons hγ S t,
-      ∃ V ≥ S, ∃ hV : V ∈ χ,
-      u ∈ Pretangle.ofCoe
-        (toPretangle (β : IicBot α) ((χ.decode V).get hV)) γ (coe_lt_coe.mpr hγ)} =
-    Pretangle.ofCoe (toPretangle (β : IicBot α) t) γ (coe_lt_coe.mpr hγ) := by
-  ext u
-  constructor
-  · simp only [ge_iff_le, mem_setOf_eq, forall_exists_index, and_imp]
-    intro χ hχ V hUV hVχ hu
-    obtain ⟨v, hv, rfl⟩ := hχ
-    rw [raiseSingleton, CodingFunction.mem_code] at hVχ
-    obtain ⟨ρ, rfl⟩ := hVχ
-    simp_rw [CodingFunction.decode_smul, raiseSingleton, CodingFunction.code_decode] at hu
-    rw [Part.get_some, toPretangle_smul, Allowable.toStructPerm_smul, StructPerm.ofCoe_smul,
-      singleton_toPretangle, smul_set_singleton, mem_singleton_iff] at hu
-    subst hu
-    rw [← mem_inv_smul_set_iff, Tree.comp_inv, ← StructPerm.ofCoe_smul, ← map_inv,
-      ← Allowable.toStructPerm_smul, ← toPretangle_smul (β : IicBot α),
-      ← hSt _ (smul_reducedSupport_eq hγ S v ρ hUV), inv_smul_smul]
-    exact hv
-  · simp only [ge_iff_le, mem_setOf_eq]
-    intro hu
-    obtain ⟨u, rfl⟩ := eq_toPretangle_of_mem β γ (coe_lt_coe.mpr hγ) t u hu
-    refine ⟨_, ⟨u, hu, rfl⟩, raisedSupport hγ S u, ?_⟩
-    refine ⟨le_raisedSupport hγ S u, CodingFunction.mem_code_self, ?_⟩
-    simp only [raiseSingleton, CodingFunction.mem_code_self, CodingFunction.code_decode,
-      Part.get_some]
-    rw [singleton_toPretangle, mem_singleton_iff]
-
-theorem appearsRaised_raiseSingletons (S : OrdSupport β) (t : Tangle β)
-    (hSt : Supports (Allowable β) {c | c ∈ S} t) :
-    AppearsRaised hγ (raiseSingletons hγ S t) S :=
-  ⟨t, raiseSingletons_reducedSupport hγ S t hSt⟩
-
-theorem decodeRaised_raiseSingletons (S : OrdSupport β) (t : Tangle β)
-    (hSt : Supports (Allowable β) {c | c ∈ S} t) :
-    decodeRaised hγ (raiseSingletons hγ S t) S (appearsRaised_raiseSingletons hγ S t hSt) = t := by
-  refine toPretangle_ext β γ hγ _ _ ?_
-  intro u
-  rw [decodeRaised_spec, raiseSingletons_reducedSupport hγ S t hSt]
-
-noncomputable def raisedCodingFunction (χs : Set (CodingFunction β))
-    (o : OrdSupportOrbit β) (ho : ∀ U ∈ o, AppearsRaised hγ χs U)
-    (ho' : ∀ U, ∀ hU : U ∈ o,
-      Supports (Allowable β) {c | c ∈ U} (decodeRaised hγ χs U (ho U hU))) :
-    CodingFunction β where
-  decode U := ⟨U ∈ o, fun hU => decodeRaised hγ χs U (ho U hU)⟩
-  dom_nonempty := o.nonempty
-  supports_decode' := ho'
-  dom_iff := by
-    intro S T hS
-    cases OrdSupportOrbit.eq_mk_of_mem hS
-    simp only [OrdSupportOrbit.mem_mk_iff, mem_orbit_iff, eq_comm]
-  decode_smul' := by
-    intro S ρ h₁ h₂
-    dsimp only
-    rw [decodeRaised_smul]
-
-theorem decode_raisedCodingFunction (χs : Set (CodingFunction β))
-    (o : OrdSupportOrbit β) (ho : ∀ U ∈ o, AppearsRaised hγ χs U)
-    (ho' : ∀ U, ∀ hU : U ∈ o,
-      Supports (Allowable β) {c | c ∈ U} (decodeRaised hγ χs U (ho U hU)))
-    (U : OrdSupport β) (hU : U ∈ raisedCodingFunction hγ χs o ho ho') :
-    ((raisedCodingFunction hγ χs o ho ho').decode U).get hU =
-    decodeRaised hγ χs U (ho U hU) :=
-  rfl
-
-theorem mem_raisedCodingFunction_iff (χs : Set (CodingFunction β))
-    (o : OrdSupportOrbit β) (ho : ∀ U ∈ o, AppearsRaised hγ χs U)
-    (ho' : ∀ U, ∀ hU : U ∈ o,
-      Supports (Allowable β) {c | c ∈ U} (decodeRaised hγ χs U (ho U hU)))
-    (U : OrdSupport β) :
-    U ∈ raisedCodingFunction hγ χs o ho ho' ↔ U ∈ o :=
-  Iff.rfl
-
-theorem raisedCodingFunction_strong {χs : Set (RaisedSingleton hγ)}
-    {o : OrdSupportOrbit β} {ho : ∀ U ∈ o, AppearsRaised hγ (Subtype.val '' χs) U}
-    {ho' : ∀ U, ∀ hU : U ∈ o,
-      Supports (Allowable β) {c | c ∈ U} (decodeRaised hγ (Subtype.val '' χs) U (ho U hU))}
-    (h : o.Strong) :
-    (raisedCodingFunction hγ (Subtype.val '' χs) o ho ho').Strong := by
-  obtain ⟨S, rfl, hS⟩ := h
-  exact ⟨S, rfl, hS⟩
-
-theorem appearsRaised_of_mem_orbit (S : OrdSupport β) (t : Tangle β)
-    (hSt : Supports (Allowable β) {c | c ∈ S} t) (U : OrdSupport β)
-    (hU : U ∈ OrdSupportOrbit.mk S) :
-    AppearsRaised hγ (raiseSingletons hγ S t) U := by
-  simp only [OrdSupportOrbit.mem_mk_iff] at hU
-  obtain ⟨ρ, rfl⟩ := hU
-  exact appearsRaised_smul hγ _ (appearsRaised_raiseSingletons hγ S t hSt) _
-
-theorem supports_decodeRaised_of_mem_orbit (S : OrdSupport β) (t : Tangle β)
-    (hSt : Supports (Allowable β) {c | c ∈ S} t) (U : OrdSupport β)
-    (hU : U ∈ OrdSupportOrbit.mk S) :
-    Supports (Allowable β) {c | c ∈ U}
-      (decodeRaised hγ (raiseSingletons hγ S t) U
-        (appearsRaised_of_mem_orbit hγ S t hSt U hU)) := by
-  simp only [OrdSupportOrbit.mem_mk_iff] at hU
-  obtain ⟨ρ₁, rfl⟩ := hU
-  intro ρ₂ hρ₂
-  rw [decodeRaised_smul hγ _ (appearsRaised_of_mem_orbit hγ S t hSt _ rfl),
-    decodeRaised_raiseSingletons hγ S t hSt]
-  rw [← inv_smul_eq_iff, smul_smul, smul_smul]
-  refine hSt _ ?_
-  intros c hc
-  rw [mul_smul, mul_smul, inv_smul_eq_iff]
-  refine hρ₂ ?_
-  dsimp only
-  simp only [OrdSupport.smul_mem, mem_setOf_eq, inv_smul_smul]
-  exact hc
-
-/-- Converts a tangle to a coding class by going via `raisedCodingFunction γ`. -/
-noncomputable def recode (S : OrdSupport β) (t : Tangle β)
-    (hSt : Supports (Allowable β) {c | c ∈ S} t) :
-    CodingFunction β :=
-  raisedCodingFunction hγ (raiseSingletons hγ S t)
-    (OrdSupportOrbit.mk S)
-    (appearsRaised_of_mem_orbit hγ S t hSt)
-    (supports_decodeRaised_of_mem_orbit hγ S t hSt)
-
-theorem decode_recode (S : OrdSupport β) (t : Tangle β)
-    (hSt : Supports (Allowable β) {c | c ∈ S} t) :
-    ((recode hγ S t hSt).decode _).get rfl = t := by
-  unfold recode
-  rw [decode_raisedCodingFunction, decodeRaised_raiseSingletons hγ S t hSt]
-
-/-- The `recode` function yields the original coding function on `t`. -/
-theorem recode_eq (S : OrdSupport β) (t : Tangle β)
-    (hSt : Supports (Allowable β) {c | c ∈ S} t) :
-    recode hγ S t hSt = CodingFunction.code S t hSt := by
-  refine CodingFunction.ext S ?_ ?_ ?_
-  · rfl
-  · exact CodingFunction.mem_code_self
-  · simp only [Support.carrier_eq_coe, CodingFunction.code_decode, Part.get_some, decode_recode]
-
-end ConNF
diff --git a/ConNF/Counting/Spec.lean b/ConNF/Counting/Spec.lean
deleted file mode 100644
index 99ed82bea2..0000000000
--- a/ConNF/Counting/Spec.lean
+++ /dev/null
@@ -1,319 +0,0 @@
-import ConNF.Foa.Basic.Flexible
-import ConNF.Counting.CodingFunction
-
-/-!
-# Specifications
--/
-
-open Ordinal Quiver Set Sum WithBot
-
-open scoped Classical Cardinal
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions] [FoaAssumptions α] {β : Iic α}
-
--- TODO: Make `Inflexible*Path` have better names.
-inductive SpecCondition (β : Iic α)
-  | atom (A : ExtendedIndex β) (i : Ordinal.{u})
-  | flexible (A : ExtendedIndex β)
-  | inflexibleCoe (A : ExtendedIndex β) (h : InflexibleCoePath A)
-      (χ : CodingFunction (h.δ : Iic α)) (hχ : χ.Strong)
-  | inflexibleBot (A : ExtendedIndex β) (h : InflexibleBotPath A) (i : Ordinal.{u})
-
-theorem SpecCondition.atom_injective {A : ExtendedIndex β} {i j : Ordinal}
-    (h : SpecCondition.atom A i = SpecCondition.atom A j) : i = j := by
-  cases h
-  rfl
-
-theorem SpecCondition.inflexibleBot_injective {A : ExtendedIndex β} {h₁ h₂ : InflexibleBotPath A}
-    {i j : Ordinal} (h : SpecCondition.inflexibleBot A h₁ i = SpecCondition.inflexibleBot A h₂ j) :
-    h₁ = h₂ ∧ i = j := by
-  cases h
-  exact ⟨rfl, rfl⟩
-
-theorem SpecCondition.inflexibleCoe_injective₁ {A : ExtendedIndex β} {h₁ h₂ : InflexibleCoePath A}
-    {χ₁ : CodingFunction h₁.δ} {χ₂ : CodingFunction h₂.δ} {hχ₁ : χ₁.Strong} {hχ₂ : χ₂.Strong}
-    (h : SpecCondition.inflexibleCoe A h₁ χ₁ hχ₁ = SpecCondition.inflexibleCoe A h₂ χ₂ hχ₂) :
-    h₁ = h₂ := by
-  cases h
-  exact rfl
-
-theorem SpecCondition.inflexibleCoe_injective₂ {A : ExtendedIndex β} {h : InflexibleCoePath A}
-    {χ₁ χ₂ : CodingFunction h.δ} {hχ₁ : χ₁.Strong} {hχ₂ : χ₂.Strong}
-    (h : SpecCondition.inflexibleCoe A h χ₁ hχ₁ = SpecCondition.inflexibleCoe A h χ₂ hχ₂) :
-    χ₁ = χ₂ := by
-  cases h
-  exact rfl
-
-@[ext]
-structure Spec (β : Iic α) where
-  orderType : Ordinal.{u}
-  cond : (i : Ordinal) → i < orderType → SpecCondition β
-
-namespace Spec
-
-/-- A specification `σ` specifies an ordered support `S` if each support condition in `S` is
-described in a sensible way by `σ`. -/
-structure Specifies (σ : Spec β) (S : OrdSupport β) : Prop where
-  lt_orderType (c : S) : typein S.r c < σ.orderType
-  of_lt_orderType (i : Ordinal) : i < σ.orderType → ∃ c : S, i = typein S.r c
-  atom_dom (A : ExtendedIndex β) (a : Atom) (ha : ⟨A, inl a⟩ ∈ S) :
-    ∃ N : NearLitter, a ∈ N ∧ ⟨A, inr N⟩ ∈ S
-  atom_spec (A : ExtendedIndex β) (a : Atom) (N : NearLitter)
-    (ha : ⟨A, inl a⟩ ∈ S) (hN : ⟨A, inr N⟩ ∈ S) : a ∈ N →
-    σ.cond (typein S.r ⟨_, ha⟩) (lt_orderType ⟨_, ha⟩) =
-    SpecCondition.atom A (typein S.r ⟨_, hN⟩)
-  flexible_spec (A : ExtendedIndex β) (N : NearLitter) (hN : ⟨A, inr N⟩ ∈ S) : Flexible α A N.fst →
-    σ.cond (typein S.r ⟨_, hN⟩) (lt_orderType ⟨_, hN⟩) = SpecCondition.flexible A
-  inflexibleCoe_spec (A : ExtendedIndex β) (N : NearLitter) (hN : ⟨A, inr N⟩ ∈ S)
-    (h : InflexibleCoe A N.1) :
-    ∃ χ : CodingFunction h.path.δ,
-    ∃ hχ : χ.Strong,
-    ∃ h' : (S.before (typein S.r ⟨_, hN⟩)).comp h.path.δ (h.path.B.cons h.path.hδ) ∈ χ,
-    (χ.decode _).get h' = h.t ∧
-    σ.cond (typein S.r ⟨_, hN⟩) (lt_orderType ⟨_, hN⟩) =
-    SpecCondition.inflexibleCoe A h.path χ hχ
-  inflexibleBot_spec (A : ExtendedIndex β) (N : NearLitter) (hN : ⟨A, inr N⟩ ∈ S)
-    (h : InflexibleBot A N.1) :
-    ∃ ha : ⟨h.path.B.cons (bot_lt_coe _), inl h.a⟩ ∈ S,
-    σ.cond (typein S.r ⟨_, hN⟩) (lt_orderType ⟨_, hN⟩) =
-    SpecCondition.inflexibleBot A h.path (typein S.r ⟨_, ha⟩)
-
-theorem orderType_eq_of_specifies {σ : Spec β} {S : OrdSupport β} (hσS : σ.Specifies S) :
-    σ.orderType = type S.r := by
-  obtain (h | h | h) := lt_trichotomy σ.orderType (type S.r)
-  · exfalso
-    obtain ⟨c, hc⟩ := typein_surj S.r h
-    exact (hσS.lt_orderType c).ne hc
-  · exact h
-  · exfalso
-    obtain ⟨c, hc⟩ := hσS.of_lt_orderType _ h
-    exact (typein_lt_type S.r c).ne hc.symm
-
-theorem specifies_subsingleton (S : OrdSupport β) :
-    {σ | Specifies σ S}.Subsingleton := by
-  rintro ⟨o, c₁⟩ h₁ ⟨_, c₂⟩ h₂
-  cases (orderType_eq_of_specifies h₂).trans (orderType_eq_of_specifies h₁).symm
-  refine Spec.ext _ _ rfl (heq_of_eq ?_)
-  dsimp only
-  funext i hi
-  obtain ⟨⟨c, hc⟩, rfl⟩ := h₁.of_lt_orderType i hi
-  obtain ⟨A, a | N⟩ := c
-  · obtain ⟨N, hN₁, hN₂⟩ := h₁.atom_dom A a hc
-    exact (h₁.atom_spec A a N hc hN₂ hN₁).trans (h₂.atom_spec A a N hc hN₂ hN₁).symm
-  obtain (hL | ⟨⟨hL⟩⟩ | ⟨⟨hL⟩⟩) := flexible_cases' β A N.1
-  · exact (h₁.flexible_spec A N hc hL).trans (h₂.flexible_spec A N hc hL).symm
-  · obtain ⟨ha₁, ha₁'⟩ := h₁.inflexibleBot_spec A N hc hL
-    obtain ⟨ha₂, ha₂'⟩ := h₂.inflexibleBot_spec A N hc hL
-    exact ha₁'.trans ha₂'.symm
-  · obtain ⟨χ₁, hχ₁, hχ₁', ht₁, h₁'⟩ := h₁.inflexibleCoe_spec A N hc hL
-    obtain ⟨χ₂, hχ₂, hχ₂', ht₂, h₂'⟩ := h₂.inflexibleCoe_spec A N hc hL
-    suffices : χ₁ = χ₂
-    · subst this
-      exact h₁'.trans h₂'.symm
-    refine CodingFunction.ext _ hχ₁' hχ₂' ?_
-    rw [ht₁, ht₂]
-
-theorem before_comp_supports {S : OrdSupport β} (hS : S.Strong)
-    {A : ExtendedIndex β} {N : NearLitter} (h : InflexibleCoe A N.1) (hN : ⟨A, inr N⟩ ∈ S) :
-    MulAction.Supports (Allowable h.path.δ)
-      {c | c ∈ (S.before (typein S.r ⟨_, hN⟩)).comp
-        h.path.δ (h.path.B.cons h.path.hδ)} h.t := by
-  intro ρ hρ
-  refine (reducedSupport α h.t).supports ?_ ?_
-  intros c hc
-  refine hρ ?_
-  rw [mem_setOf, OrdSupport.mem_comp (h.path.δ : Iic α), OrdSupport.mem_before]
-  refine ⟨?_, ?_⟩
-  · refine hS.transConstrains_mem _ ⟨⟨A, inr N⟩, hN⟩ ?_ ?_
-    · exact hc.2
-    · obtain ⟨d, hd₁, hd₂⟩ := hc.1
-      refine Relation.TransGen.trans_right (reflTransConstrains_comp hd₂ _) ?_
-      refine transConstrains_nearLitter ?_
-      have := Constrains.fuzz h.path.hδ h.path.hε h.path.hδε h.path.B h.t d hd₁
-      rw [← h.path.hA, ← h.hL] at this
-      exact Relation.TransGen.single this
-  · simp only [OrdSupport.coe_sort_coe, typein_lt_typein]
-    refine hS.lt_of_transConstrains _ _ ?_
-    have := transConstrains_of_mem_reducedSupport α h.path.hδ h.path.hε h.path.hδε h.path.B h.t c hc
-    rw [← h.path.hA, ← h.hL] at this
-    exact transConstrains_nearLitter this
-
-noncomputable def codeBefore {S : OrdSupport β} (hS : S.Strong)
-    {A : ExtendedIndex β} {N : NearLitter} (h : InflexibleCoe A N.1) (hN : ⟨A, inr N⟩ ∈ S) :
-    CodingFunction (h.path.δ : Iic α) :=
-  CodingFunction.code
-    ((S.before (typein S.r ⟨_, hN⟩)).comp h.path.δ (h.path.B.cons h.path.hδ))
-    h.t (before_comp_supports hS h hN)
-
-theorem codeBefore_strong {S : OrdSupport β} (hS : S.Strong)
-    {A : ExtendedIndex β} {N : NearLitter} (h : InflexibleCoe A N.1) (hN : ⟨A, inr N⟩ ∈ S) :
-    (codeBefore hS h hN).Strong :=
-  CodingFunction.code_strong ((hS.before _).comp _ _)
-
-noncomputable def specCondition {S : OrdSupport β} (hS : S.Strong) :
-    (c : S) → SpecCondition β
-  | ⟨⟨A, Sum.inl a⟩, hc⟩ => SpecCondition.atom A
-      (typein S.r ⟨⟨A, inr a.1.toNearLitter⟩, hS.transConstrains_mem _ ⟨_, hc⟩
-        (Reduced.mkLitter _) (Relation.TransGen.single <| Constrains.atom _ _)⟩)
-  | ⟨⟨A, Sum.inr N⟩, hc⟩ =>
-      if h : Nonempty (InflexibleCoe A N.1) then
-        SpecCondition.inflexibleCoe A h.some.path
-          (codeBefore hS h.some hc) (codeBefore_strong hS h.some hc)
-      else if h : Nonempty (InflexibleBot A N.1) then
-        SpecCondition.inflexibleBot A h.some.path
-          (typein S.r ⟨⟨h.some.path.B.cons (bot_lt_coe _), inl h.some.a⟩,
-            hS.transConstrains_mem _ ⟨_, hc⟩ (Reduced.mkAtom _)
-            (by
-              have := Constrains.fuzz_bot h.some.path.hε h.some.path.B h.some.a
-              rw [← h.some.path.hA, ← h.some.hL] at this
-              exact transConstrains_nearLitter (Relation.TransGen.single this))⟩)
-      else
-        SpecCondition.flexible A
-
-@[simp]
-theorem specCondition_atom {S : OrdSupport β} {hS : S.Strong}
-    (A : ExtendedIndex β) (a : Atom) (h : ⟨A, inl a⟩ ∈ S) :
-    specCondition hS ⟨⟨A, inl a⟩, h⟩ = SpecCondition.atom A
-      (typein S.r ⟨⟨A, inr a.1.toNearLitter⟩, hS.transConstrains_mem _ ⟨_, h⟩
-        (Reduced.mkLitter _) (Relation.TransGen.single <| Constrains.atom _ _)⟩) :=
-  rfl
-
-theorem specCondition_inflexibleCoe {S : OrdSupport β} {hS : S.Strong}
-    (A : ExtendedIndex β) (N : NearLitter) (hNS : ⟨A, inr N⟩ ∈ S) (hN : InflexibleCoe A N.1) :
-    specCondition hS ⟨⟨A, inr N⟩, hNS⟩ =
-    SpecCondition.inflexibleCoe A hN.path (codeBefore hS hN hNS) (codeBefore_strong hS hN hNS) := by
-  rw [specCondition]
-  dsimp only
-  rw [dif_pos ⟨hN⟩]
-  have : hN = Nonempty.some ⟨hN⟩ := Subsingleton.elim _ _
-  rw [this]
-
-theorem specCondition_inflexibleBot {S : OrdSupport β} {hS : S.Strong}
-    (A : ExtendedIndex β) (N : NearLitter) (hNS : ⟨A, inr N⟩ ∈ S) (hN : InflexibleBot A N.1)
-    (ha : ⟨hN.path.B.cons (bot_lt_coe _), inl hN.a⟩ ∈ S) :
-    specCondition hS ⟨⟨A, inr N⟩, hNS⟩ =
-    SpecCondition.inflexibleBot A hN.path
-      (typein S.r ⟨⟨hN.path.B.cons (bot_lt_coe _), inl hN.a⟩, ha⟩) := by
-  rw [specCondition]
-  dsimp only
-  rw [dif_neg, dif_pos ⟨hN⟩]
-  · have : hN = Nonempty.some ⟨hN⟩ := Subsingleton.elim _ _
-    congr 2
-    · rw [this]
-    · simp only [OrdSupport.coe_sort_coe, Subtype.mk.injEq, SupportCondition.mk.injEq, inl.injEq]
-      rw [this]
-      exact ⟨rfl, rfl⟩
-  · rintro ⟨hN'⟩
-    exact inflexibleBot_inflexibleCoe hN hN'
-
-theorem specCondition_flexible {S : OrdSupport β} {hS : S.Strong}
-    (A : ExtendedIndex β) (N : NearLitter) (hNS : ⟨A, inr N⟩ ∈ S) (hN : Flexible α A N.1) :
-    specCondition hS ⟨⟨A, inr N⟩, hNS⟩ = SpecCondition.flexible A := by
-  rw [specCondition]
-  dsimp only
-  rw [flexible_iff_not_inflexibleBot_inflexibleCoe] at hN
-  rw [dif_neg, dif_neg]
-  · exact not_nonempty_iff.mpr hN.1
-  · exact not_nonempty_iff.mpr hN.2
-
-/-- The support condition at position `i` in `S`. -/
-noncomputable def _root_.ConNF.OrdSupport.conditionAt (S : OrdSupport β)
-    (i : Ordinal) (hi : i < type S.r) : S :=
-  (typein_surj S.r hi).choose
-
-@[simp]
-theorem typein_conditionAt (S : OrdSupport β) (i : Ordinal) (hi : i < type S.r) :
-    typein S.r (S.conditionAt i hi) = i :=
-  (typein_surj S.r hi).choose_spec
-
-@[simp]
-theorem conditionAt_typein (S : OrdSupport β) (c : S) :
-    S.conditionAt (typein S.r c) (typein_lt_type S.r c) = c := by
-  refine typein_injective S.r ?_
-  rw [typein_conditionAt]
-
-noncomputable def spec (S : OrdSupport β) (hS : S.Strong) : Spec β where
-  orderType := type S.r
-  cond i hi := specCondition hS (S.conditionAt i hi)
-
-@[simp]
-theorem spec_orderType {S : OrdSupport β} {hS : S.Strong} :
-    (spec S hS).orderType = type S.r :=
-  rfl
-
-@[simp]
-theorem spec_cond_eq {S : OrdSupport β} {hS : S.Strong}
-    (i : Ordinal) (hi : i < type S.r) :
-    (spec S hS).cond i hi = specCondition hS (S.conditionAt i hi) :=
-  rfl
-
-/-- Every strong support has a specification, described by `spec`. -/
-theorem spec_specifies {S : OrdSupport β} (hS : S.Strong) :
-    (spec S hS).Specifies S := by
-  constructor
-  case lt_orderType =>
-    intro c
-    simp only [OrdSupport.coe_sort_coe, spec_orderType]
-    exact typein_lt_type S.r c
-  case of_lt_orderType =>
-    intro i hi
-    simp only [OrdSupport.coe_sort_coe, Subtype.exists]
-    obtain ⟨c, hc⟩ := typein_surj S.r hi
-    exact ⟨c, c.prop, hc.symm⟩
-  case atom_dom =>
-    intro A a ha
-    refine ⟨a.1.toNearLitter, rfl, ?_⟩
-    refine hS.transConstrains_mem _ ⟨_, ha⟩ (Reduced.mkLitter _) ?_
-    exact Relation.TransGen.single (Constrains.atom _ _)
-  case atom_spec =>
-    intro A a N ha hN haN
-    simp only [OrdSupport.coe_sort_coe, spec_cond_eq, conditionAt_typein, specCondition_atom,
-      SpecCondition.atom.injEq, typein_inj, Subtype.mk.injEq, SupportCondition.mk.injEq,
-      inr.injEq, true_and]
-    have := hS.reduced_of_mem ⟨_, hN⟩
-    cases this
-    cases haN
-    rfl
-  case flexible_spec =>
-    intro A N hN₁ hN₂
-    simp only [OrdSupport.coe_sort_coe, spec_cond_eq, conditionAt_typein]
-    rw [specCondition_flexible A N hN₁ hN₂]
-  case inflexibleCoe_spec =>
-    intro A N hN₁ hN₂
-    refine ⟨codeBefore hS hN₂ hN₁, codeBefore_strong hS hN₂ hN₁, ?_, ?_, ?_⟩
-    · rw [codeBefore]
-      exact CodingFunction.mem_code_self
-    · simp only [codeBefore, CodingFunction.code_decode, Part.get_some]
-    · simp only [OrdSupport.coe_sort_coe, spec_cond_eq, conditionAt_typein]
-      rw [specCondition_inflexibleCoe A N hN₁ hN₂]
-  case inflexibleBot_spec =>
-    intro A N hN₁ hN₂
-    refine ⟨?_, ?_⟩
-    · refine hS.transConstrains_mem _ ⟨_, hN₁⟩ (Reduced.mkAtom _) ?_
-      have := Constrains.fuzz_bot hN₂.path.hε hN₂.path.B hN₂.a
-      rw [← hN₂.hL, ← hN₂.path.hA] at this
-      exact transConstrains_nearLitter (Relation.TransGen.single this)
-    · simp only [OrdSupport.coe_sort_coe, spec_cond_eq, conditionAt_typein]
-      rw [specCondition_inflexibleBot A N hN₁ hN₂]
-
-/-- A specification is *strong* if it specifies a strong support. -/
-def Strong (σ : Spec β) : Prop :=
-  ∃ S : OrdSupport β, S.Strong ∧ σ.Specifies S
-
-/-- A strong support specified by this strong specification. -/
-noncomputable def Strong.out {σ : Spec β} (h : σ.Strong) : OrdSupport β :=
-  h.choose
-
-theorem Strong.out_strong {σ : Spec β} (h : σ.Strong) : h.out.Strong :=
-  h.choose_spec.1
-
-theorem Strong.specifies_out {σ : Spec β} (h : σ.Strong) : σ.Specifies h.out :=
-  h.choose_spec.2
-
-end Spec
-
-end ConNF
diff --git a/ConNF/Counting/SpecSame.lean b/ConNF/Counting/SpecSame.lean
deleted file mode 100644
index 9cd2004809..0000000000
--- a/ConNF/Counting/SpecSame.lean
+++ /dev/null
@@ -1,871 +0,0 @@
-import ConNF.Foa
-import ConNF.Counting.Spec
-
-/-!
-# Specifying two strong supports at once
--/
-
-open Ordinal Quiver Set Sum WithBot
-
-open scoped Classical
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] {α : Λ} [BasePositions] [FoaAssumptions α] {β : Iic α}
-  {σ : Spec β} {S T : OrdSupport β}
-  (hσS : σ.Specifies S) (hσT : σ.Specifies T) (hS : S.Strong) (hT : T.Strong)
-
-namespace Spec
-
-theorem type_eq_type : type S.r = type T.r :=
-  by rw [← orderType_eq_of_specifies hσS, ← orderType_eq_of_specifies hσT]
-
-theorem typein_lt {c : S} :
-    typein S.r c < σ.orderType :=
-  orderType_eq_of_specifies hσS ▸ typein_lt_type S.r _
-
-noncomputable def convertCondition (c : S) : T :=
-  T.conditionAt (typein S.r c) (type_eq_type hσS hσT ▸ typein_lt_type S.r c)
-
-@[simp]
-theorem typein_convertCondition (c : S) :
-    typein T.r (convertCondition hσS hσT c) = typein S.r c :=
-  by rw [convertCondition, typein_conditionAt]
-
-theorem convertCondition_eq_of_typein_eq {c : S} {d : T}
-    (hb : typein S.r c = typein T.r d) :
-    convertCondition hσS hσT c = d := by
-  refine typein_injective T.r ?_
-  rw [← hb, typein_convertCondition]
-
-@[simp]
-theorem convertCondition_lt (c d : S) :
-    convertCondition hσS hσT c < convertCondition hσS hσT d ↔ c < d := by
-  refine (typein_lt_typein T.r).symm.trans ?_
-  simp only [OrdSupport.coe_sort_coe, typein_convertCondition, typein_lt_typein]
-  rfl
-
-@[simp]
-theorem convertCondition_convertCondition (c : S) :
-    convertCondition hσT hσS (convertCondition hσS hσT c) = c := by
-  refine typein_injective S.r ?_
-  simp only [typein_convertCondition]
-
-theorem convertCondition_atom (A : ExtendedIndex β) (a : Atom) (h : ⟨A, inl a⟩ ∈ S) :
-    ∃ b : Atom, ∃ hb : ⟨A, inl b⟩ ∈ T,
-      convertCondition hσS hσT ⟨⟨A, inl a⟩, h⟩ = ⟨⟨A, inl b⟩, hb⟩ := by
-  have hc_spec := hσS.atom_spec A a a.1.toNearLitter h
-    (hS.transConstrains_mem _ ⟨_, h⟩ (Reduced.mkLitter _)
-      (Relation.TransGen.single <| Constrains.atom _ _)) rfl
-  set d := convertCondition hσS hσT ⟨⟨A, inl a⟩, h⟩ with hd
-  obtain ⟨⟨B, b | N⟩, hdT⟩ := d
-  · have hd_spec := hσT.atom_spec B b b.1.toNearLitter hdT
-      (hT.transConstrains_mem _ ⟨_, hdT⟩ (Reduced.mkLitter _)
-        (Relation.TransGen.single <| Constrains.atom _ _)) rfl
-    simp_rw [hd] at hd_spec
-    simp only [OrdSupport.coe_sort_coe, typein_convertCondition,
-      hc_spec, SpecCondition.atom.injEq] at hd_spec
-    cases hd_spec.1
-    exact ⟨b, hdT, rfl⟩
-  exfalso
-  obtain (hL | ⟨⟨hL⟩⟩ | ⟨⟨hL⟩⟩) := flexible_cases' β B N.1
-  · have hd_spec := hσT.flexible_spec B N hdT hL
-    simp_rw [hd] at hd_spec
-    simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec] at hd_spec
-  · obtain ⟨hdT', hd_spec⟩ := hσT.inflexibleBot_spec B N hdT hL
-    simp_rw [hd] at hd_spec
-    simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec] at hd_spec
-  · obtain ⟨χ, hχ₁, hχ₂, hd_spec⟩ := hσT.inflexibleCoe_spec B N hdT hL
-    simp_rw [hd] at hd_spec
-    simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec, and_false] at hd_spec
-
-noncomputable def convertAtom (A : ExtendedIndex β) (a : Atom) (h : ⟨A, inl a⟩ ∈ S) : Atom :=
-  (convertCondition_atom hσS hσT hS hT A a h).choose
-
-theorem convertAtom_mem (A : ExtendedIndex β) (a : Atom) (h : ⟨A, inl a⟩ ∈ S) :
-    ⟨A, inl (convertAtom hσS hσT hS hT A a h)⟩ ∈ T :=
-  (convertCondition_atom hσS hσT hS hT A a h).choose_spec.1
-
-theorem convertCondition_eq_convertAtom (A : ExtendedIndex β) (a : Atom) (h : ⟨A, inl a⟩ ∈ S) :
-    convertCondition hσS hσT ⟨⟨A, inl a⟩, h⟩ =
-    ⟨⟨A, inl (convertAtom hσS hσT hS hT A a h)⟩, (convertAtom_mem hσS hσT hS hT A a h)⟩ :=
-  (convertCondition_atom hσS hσT hS hT A a h).choose_spec.2
-
-theorem convertCondition_litter (A : ExtendedIndex β) (L : Litter)
-    (h : ⟨A, inr L.toNearLitter⟩ ∈ S) :
-    ∃ L' : Litter, ∃ hL' : ⟨A, inr L'.toNearLitter⟩ ∈ T,
-      convertCondition hσS hσT ⟨⟨A, inr L.toNearLitter⟩, h⟩ = ⟨⟨A, inr L'.toNearLitter⟩, hL'⟩ := by
-  set d := convertCondition hσS hσT ⟨⟨A, inr L.toNearLitter⟩, h⟩ with hd
-  obtain ⟨⟨B, b | N⟩, hdT⟩ := d
-  · exfalso
-    have hd_spec := hσT.atom_spec B b b.1.toNearLitter hdT
-      (hT.transConstrains_mem _ ⟨_, hdT⟩ (Reduced.mkLitter _)
-        (Relation.TransGen.single <| Constrains.atom _ _)) rfl
-    simp_rw [hd] at hd_spec
-    obtain (hL | ⟨⟨hL⟩⟩ | ⟨⟨hL⟩⟩) := flexible_cases' β A L
-    · have hc_spec := hσS.flexible_spec A L.toNearLitter h hL
-      simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec] at hd_spec
-    · obtain ⟨hL, hc_spec⟩ := hσS.inflexibleBot_spec A L.toNearLitter h hL
-      simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec] at hd_spec
-    · obtain ⟨χ, _, _, hc_spec⟩ := hσS.inflexibleCoe_spec A L.toNearLitter h hL
-      simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec] at hd_spec
-  obtain ⟨L', rfl⟩ := (isLitter_of_reduced (hT.reduced_of_mem ⟨_, hdT⟩)).exists_litter_eq
-  obtain (hL₂ | ⟨⟨hL₂⟩⟩ | ⟨⟨hL₂⟩⟩) := flexible_cases' β B L'
-  · have hd_spec := hσT.flexible_spec B L'.toNearLitter hdT hL₂
-    simp_rw [hd] at hd_spec
-    obtain (hL₁ | ⟨⟨hL₁⟩⟩ | ⟨⟨hL₁⟩⟩) := flexible_cases' β A L
-    · have hc_spec := hσS.flexible_spec A L.toNearLitter h hL₁
-      simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec,
-        SpecCondition.flexible.injEq] at hd_spec
-      cases hd_spec
-      exact ⟨L', hdT, rfl⟩
-    · obtain ⟨hL, hc_spec⟩ := hσS.inflexibleBot_spec A L.toNearLitter h hL₁
-      simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec] at hd_spec
-    · obtain ⟨χ, _, _, hc_spec⟩ := hσS.inflexibleCoe_spec A L.toNearLitter h hL₁
-      simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec] at hd_spec
-  · obtain ⟨hdT', hd_spec⟩ := hσT.inflexibleBot_spec B L'.toNearLitter hdT hL₂
-    simp_rw [hd] at hd_spec
-    obtain (hL₁ | ⟨⟨hL₁⟩⟩ | ⟨⟨hL₁⟩⟩) := flexible_cases' β A L
-    · have hc_spec := hσS.flexible_spec A L.toNearLitter h hL₁
-      simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec] at hd_spec
-    · obtain ⟨hL, hc_spec⟩ := hσS.inflexibleBot_spec A L.toNearLitter h hL₁
-      simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec, Litter.toNearLitter_fst,
-        SpecCondition.inflexibleBot.injEq] at hd_spec
-      cases hd_spec.1
-      exact ⟨L', hdT, rfl⟩
-    · obtain ⟨χ, _, _, hc_spec⟩ := hσS.inflexibleCoe_spec A L.toNearLitter h hL₁
-      simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec] at hd_spec
-  · obtain ⟨χ, _, _, hd_spec⟩ := hσT.inflexibleCoe_spec B L'.toNearLitter hdT hL₂
-    simp_rw [hd] at hd_spec
-    obtain (hL₁ | ⟨⟨hL₁⟩⟩ | ⟨⟨hL₁⟩⟩) := flexible_cases' β A L
-    · have hc_spec := hσS.flexible_spec A L.toNearLitter h hL₁
-      simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec, and_false] at hd_spec
-    · obtain ⟨hL, hc_spec⟩ := hσS.inflexibleBot_spec A L.toNearLitter h hL₁
-      simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec, and_false] at hd_spec
-    · obtain ⟨χ, _, _, hc_spec⟩ := hσS.inflexibleCoe_spec A L.toNearLitter h hL₁
-      simp only [Litter.toNearLitter_fst, OrdSupport.coe_sort_coe, typein_convertCondition, hc_spec,
-        SpecCondition.inflexibleCoe.injEq] at hd_spec
-      cases hd_spec.2.1
-      exact ⟨L', hdT, rfl⟩
-
-noncomputable def convertLitter (A : ExtendedIndex β) (L : Litter)
-    (h : ⟨A, inr L.toNearLitter⟩ ∈ S) : Litter :=
-  (convertCondition_litter hσS hσT hT A L h).choose
-
-theorem convertLitter_mem (A : ExtendedIndex β) (L : Litter)
-    (h : ⟨A, inr L.toNearLitter⟩ ∈ S) :
-    ⟨A, inr (convertLitter hσS hσT hT A L h).toNearLitter⟩ ∈ T :=
-  (convertCondition_litter hσS hσT hT A L h).choose_spec.1
-
-theorem convertCondition_eq_convertLitter (A : ExtendedIndex β) (L : Litter)
-    (h : ⟨A, inr L.toNearLitter⟩ ∈ S) :
-    convertCondition hσS hσT ⟨⟨A, inr L.toNearLitter⟩, h⟩ =
-    ⟨⟨A, inr (convertLitter hσS hσT hT A L h).toNearLitter⟩, (convertLitter_mem hσS hσT hT A L h)⟩ :=
-  (convertCondition_litter hσS hσT hT A L h).choose_spec.2
-
-theorem convertAtom_eq_of_typein_eq {A₁ A₂ : ExtendedIndex β} {a₁ a₂ : Atom}
-    {h₁ : ⟨A₁, inl a₁⟩ ∈ S} {h₂ : ⟨A₂, inl a₂⟩ ∈ T}
-    (h : typein S.r ⟨_, h₁⟩ = typein T.r ⟨_, h₂⟩) :
-    convertAtom hσS hσT hS hT A₁ a₁ h₁ = a₂ := by
-  have := convertCondition_eq_of_typein_eq hσS hσT h
-  simp only [convertCondition_eq_convertAtom hσS hσT hS hT, Subtype.mk.injEq,
-    SupportCondition.mk.injEq, inl.injEq] at this
-  exact this.2
-
-theorem convertLitter_eq_of_typein_eq {A₁ A₂ : ExtendedIndex β} {L₁ L₂ : Litter}
-    {h₁ : ⟨A₁, inr L₁.toNearLitter⟩ ∈ S} {h₂ : ⟨A₂, inr L₂.toNearLitter⟩ ∈ T}
-    (h : typein S.r ⟨_, h₁⟩ = typein T.r ⟨_, h₂⟩) :
-    convertLitter hσS hσT hT A₁ L₁ h₁ = L₂ := by
-  have := convertCondition_eq_of_typein_eq hσS hσT h
-  simp only [convertCondition_eq_convertLitter hσS hσT hT, Subtype.mk.injEq,
-    SupportCondition.mk.injEq, inr.injEq, Litter.toNearLitter_injective.eq_iff] at this
-  exact this.2
-
-@[simp]
-theorem convertCondition_path (c : S) :
-    (convertCondition hσS hσT c).val.path = c.val.path := by
-  obtain ⟨⟨A, a | N⟩, hc⟩ := c
-  · rw [convertCondition_eq_convertAtom hσS hσT hS hT]
-  · obtain ⟨L, rfl⟩ := (isLitter_of_reduced (hS.reduced_of_mem ⟨_, hc⟩)).exists_litter_eq
-    rw [convertCondition_eq_convertLitter hσS hσT hT]
-
-@[simp]
-theorem convertCondition_mk (A : ExtendedIndex β) (x : Atom ⊕ NearLitter) (h : ⟨A, x⟩ ∈ S) :
-    ⟨A, (convertCondition hσS hσT ⟨⟨A, x⟩, h⟩).val.value⟩ =
-    (convertCondition hσS hσT ⟨⟨A, x⟩, h⟩).val := by
-  have := convertCondition_path hσS hσT hS hT ⟨⟨A, x⟩, h⟩
-  dsimp only at this
-  conv in SupportCondition.mk _ =>
-    rw [← this]
-
-@[simp]
-theorem convertAtom_convertAtom (A : ExtendedIndex β) (a : Atom) (h : ⟨A, inl a⟩ ∈ S) :
-    convertAtom hσT hσS hT hS A (convertAtom hσS hσT hS hT A a h)
-      (convertAtom_mem hσS hσT hS hT A a h) = a := by
-  have := convertCondition_convertCondition hσS hσT ⟨⟨A, inl a⟩, h⟩
-  rw [convertCondition_eq_convertAtom, convertCondition_eq_convertAtom] at this
-  simp only [Subtype.mk.injEq, SupportCondition.mk.injEq, inl.injEq, true_and] at this
-  exact this
-
-@[simp]
-theorem convertLitter_convertLitter (A : ExtendedIndex β) (L : Litter)
-    (h : ⟨A, inr L.toNearLitter⟩ ∈ S) :
-    convertLitter hσT hσS hS A (convertLitter hσS hσT hT A L h)
-      (convertLitter_mem hσS hσT hT A L h) = L := by
-  have := convertCondition_convertCondition hσS hσT ⟨⟨A, inr L.toNearLitter⟩, h⟩
-  rw [convertCondition_eq_convertLitter, convertCondition_eq_convertLitter] at this
-  simp only [Subtype.mk.injEq, SupportCondition.mk.injEq, inr.injEq, true_and,
-    Litter.toNearLitter_injective.eq_iff] at this
-  exact this
-
-theorem convertAtom_injective {A : ExtendedIndex β} {a b : Atom}
-    (ha : ⟨A, inl a⟩ ∈ S) (hb : ⟨A, inl b⟩ ∈ S)
-    (h : convertAtom hσS hσT hS hT A a ha = convertAtom hσS hσT hS hT A b hb) :
-    a = b := by
-  have := convertAtom_convertAtom hσS hσT hS hT A a ha
-  simp_rw [h, convertAtom_convertAtom] at this
-  exact this.symm
-
-theorem convertLitter_injective {A : ExtendedIndex β} {L₁ L₂ : Litter}
-    (h₁ : ⟨A, inr L₁.toNearLitter⟩ ∈ S) (h₂ : ⟨A, inr L₂.toNearLitter⟩ ∈ S)
-    (h : convertLitter hσS hσT hT A L₁ h₁ = convertLitter hσS hσT hT A L₂ h₂) :
-    L₁ = L₂ := by
-  have := convertLitter_convertLitter hσS hσT hS hT A L₁ h₁
-  simp_rw [h, convertLitter_convertLitter] at this
-  exact this.symm
-
-@[simp]
-theorem typein_convertAtom (A : ExtendedIndex β) (a : Atom) (h : ⟨A, inl a⟩ ∈ S) :
-    typein T.r ⟨⟨A, inl (convertAtom hσS hσT hS hT A a h)⟩, convertAtom_mem hσS hσT hS hT A a h⟩ =
-    typein S.r ⟨⟨A, inl a⟩, h⟩ :=
-  by rw [← convertCondition_eq_convertAtom, typein_convertCondition]
-
-@[simp]
-theorem typein_convertLitter (A : ExtendedIndex β) (L : Litter) (h : ⟨A, inr L.toNearLitter⟩ ∈ S) :
-    typein T.r ⟨⟨A, inr (convertLitter hσS hσT hT A L h).toNearLitter⟩,
-      convertLitter_mem hσS hσT hT A L h⟩ =
-    typein S.r ⟨⟨A, inr L.toNearLitter⟩, h⟩ :=
-  by rw [← convertCondition_eq_convertLitter, typein_convertCondition]
-
-noncomputable def convert : StructAction β :=
-  fun A => {
-    atomMap := fun a => ⟨_, fun h => convertAtom hσS hσT hS hT A a h⟩
-    litterMap := fun L => ⟨_, fun h => (convertLitter hσS hσT hT A L h).toNearLitter⟩
-    atomMap_dom_small := by
-      refine S.small.preimage ?_
-      intros _ _ h
-      simp only [SupportCondition.mk.injEq, inl.injEq, true_and] at h
-      exact h
-    litterMap_dom_small := by
-      refine S.small.preimage ?_
-      intros _ _ h
-      simp only [SupportCondition.mk.injEq, inr.injEq, true_and,
-        Litter.toNearLitter_injective.eq_iff] at h
-      exact h
-  }
-
-@[simp]
-theorem convert_atomMap {A : ExtendedIndex β} {a : Atom}
-    {h : (⟨A, inl a⟩ : SupportCondition β) ∈ S} :
-    ((convert hσS hσT hS hT A).atomMap a).get h = convertAtom hσS hσT hS hT A a h :=
-  rfl
-
-@[simp]
-theorem convert_litterMap {A : ExtendedIndex β} {L : Litter}
-    {h : (⟨A, inr L.toNearLitter⟩ : SupportCondition β) ∈ S} :
-    ((convert hσS hσT hS hT A).litterMap L).get h = (convertLitter hσS hσT hT A L h).toNearLitter :=
-  rfl
-
-@[simp]
-theorem _root_.ConNF.mem_toNearLitter {a : Atom} {L : Litter} :
-    a ∈ L.toNearLitter ↔ a.1 = L :=
-  Iff.rfl
-
-@[simp]
-theorem convertAtom_fst {A : ExtendedIndex β} {a : Atom}
-    (h : (⟨A, inl a⟩ : SupportCondition β) ∈ S) :
-    (convertAtom hσS hσT hS hT A a h).1 =
-    convertLitter hσS hσT hT A a.1 (hS.fst_toNearLitter_mem h) := by
-  have hσ₁ := hσS.atom_spec A a a.1.toNearLitter h (hS.fst_toNearLitter_mem h) rfl
-  have hσ₂ := hσT.atom_spec A (convertAtom hσS hσT hS hT A a h)
-    (convertAtom hσS hσT hS hT A a h).1.toNearLitter (convertAtom_mem hσS hσT hS hT A a h)
-    (hT.fst_toNearLitter_mem (convertAtom_mem hσS hσT hS hT A a h)) rfl
-  rw [← convertCondition_eq_convertAtom] at hσ₂
-  simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hσ₁, SpecCondition.atom.injEq,
-    true_and] at hσ₂
-  have := congr_arg (typein T.r)
-    (convertCondition_eq_convertLitter hσS hσT hT A a.1 (hS.fst_toNearLitter_mem h))
-  simp only [OrdSupport.coe_sort_coe, typein_convertCondition, hσ₂, typein_inj, Subtype.mk.injEq,
-    SupportCondition.mk.injEq, inr.injEq, true_and, Litter.toNearLitter_injective.eq_iff] at this
-  exact this
-
-theorem convert_lawful : StructAction.Lawful (convert hσS hσT hS hT) :=
-  fun A => {
-    atomMap_injective := fun a b ha hb h => convertAtom_injective hσS hσT hS hT ha hb h
-    litterMap_injective := by
-      intro L₁ L₂ h₁ h₂ h
-      refine convertLitter_injective hσS hσT hS hT h₁ h₂ ?_
-      obtain ⟨a, ha₁, ha₂⟩ := h
-      exact eq_of_mem_litterSet_of_mem_litterSet ha₁ ha₂
-    atom_mem := by
-      intro a ha L hL
-      simp only [convert_atomMap, convert_litterMap, mem_toNearLitter, convertAtom_fst]
-      constructor
-      · rintro rfl
-        rfl
-      · exact convertLitter_injective hσS hσT hS hT (hS.fst_toNearLitter_mem ha) hL
-  }
-
-theorem convert_mapFlexible : StructAction.MapFlexible (convert hσS hσT hS hT) := by
-  intro A L hL₁ hL₂
-  have hLS := hσS.flexible_spec A L.toNearLitter hL₁ hL₂
-  obtain (hL | ⟨⟨hL⟩⟩ | ⟨⟨hL⟩⟩) := flexible_cases' β A (convertLitter hσS hσT hT A L hL₁)
-  · exact hL
-  · exfalso
-    obtain ⟨_, hLT⟩ := hσT.inflexibleBot_spec A _ (convertLitter_mem hσS hσT hT A L hL₁) hL
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter, hLS, Litter.toNearLitter_fst] at hLT
-  · exfalso
-    obtain ⟨χ, _, _, _, hLT⟩ := hσT.inflexibleCoe_spec A _ (convertLitter_mem hσS hσT hT A L hL₁) hL
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter, hLS, Litter.toNearLitter_fst] at hLT
-
-noncomputable def convertAllowable : Allowable β :=
-  (StructApprox.freedom_of_action β
-    (StructAction.rc (convert hσS hσT hS hT) (convert_lawful hσS hσT hS hT))
-    (StructAction.rc_free _ _ (convert_mapFlexible hσS hσT hS hT))).choose
-
-theorem convertAllowable_spec :
-    (StructAction.rc (convert hσS hσT hS hT)
-      (convert_lawful hσS hσT hS hT)).ExactlyApproximates
-    (Allowable.toStructPerm (convertAllowable hσS hσT hS hT)) :=
-  (StructApprox.freedom_of_action β
-    (StructAction.rc (convert hσS hσT hS hT) (convert_lawful hσS hσT hS hT))
-    (StructAction.rc_free _ _ (convert_mapFlexible hσS hσT hS hT))).choose_spec
-
-/-- If `LawfulIn s` holds, `convertAllowable` acts on support conditions assigned at a time in `s`
-exactly as specified by `convertCondition`. -/
-structure LawfulIn (s : Set Ordinal) : Prop where
-  smul_eq : ∀ c : S, typein S.r c ∈ s →
-    convertAllowable hσS hσT hS hT • c.val = convertCondition hσS hσT c
-  inv_smul_eq : ∀ c : T, typein T.r c ∈ s →
-    (convertAllowable hσS hσT hS hT)⁻¹ • c.val = convertCondition hσT hσS c
-
-theorem LawfulIn.smul_mem {s : Set Ordinal} (h : LawfulIn hσS hσT hS hT s)
-    (c : S) (hc : typein S.r c ∈ s) :
-    convertAllowable hσS hσT hS hT • c.val ∈ T := by
-  rw [h.smul_eq c hc]
-  exact (convertCondition hσS hσT c).prop
-
-theorem LawfulIn.inv_smul_mem {s : Set Ordinal} (h : LawfulIn hσS hσT hS hT s)
-    (c : T) (hc : typein T.r c ∈ s) :
-    (convertAllowable hσS hσT hS hT)⁻¹ • c.val ∈ S := by
-  rw [h.inv_smul_eq c hc]
-  exact (convertCondition hσT hσS c).prop
-
-theorem LawfulIn.typein_smul {s : Set Ordinal} (h : LawfulIn hσS hσT hS hT s)
-    (c : S) (hc : typein S.r c ∈ s) :
-    typein T.r ⟨convertAllowable hσS hσT hS hT • c.val, h.smul_mem c hc⟩ = typein S.r c :=
-  by simp only [h.smul_eq c hc, OrdSupport.coe_sort_coe, Subtype.coe_eta, typein_convertCondition]
-
-theorem LawfulIn.typein_inv_smul {s : Set Ordinal} (h : LawfulIn hσS hσT hS hT s)
-    (c : T) (hc : typein T.r c ∈ s) :
-    typein S.r ⟨(convertAllowable hσS hσT hS hT)⁻¹ • c.val, h.inv_smul_mem c hc⟩ = typein T.r c :=
-  by simp only [h.inv_smul_eq c hc, OrdSupport.coe_sort_coe, Subtype.coe_eta,
-    typein_convertCondition]
-
-abbrev LawfulBefore (i : Ordinal) : Prop :=
-  LawfulIn hσS hσT hS hT {j | j < i}
-
-theorem lawfulIn_iff (s : Set Ordinal) :
-    LawfulIn hσS hσT hS hT s ↔ ∀ i ∈ s, LawfulIn hσS hσT hS hT {i} := by
-  constructor
-  · intro h i hi
-    constructor
-    case smul_eq =>
-      rintro c rfl
-      exact h.smul_eq c hi
-    case inv_smul_eq =>
-      rintro c rfl
-      exact h.inv_smul_eq c hi
-  · intro h
-    constructor
-    case smul_eq =>
-      intro c hcd
-      refine (h _ hcd).smul_eq c rfl
-    case inv_smul_eq =>
-      intro c hcd
-      refine (h _ hcd).inv_smul_eq c rfl
-
-theorem lawfulBefore_induction
-    (h : ∀ i, LawfulBefore hσS hσT hS hT i → LawfulIn hσS hσT hS hT {i}) :
-    LawfulIn hσS hσT hS hT univ := by
-  rw [lawfulIn_iff]
-  simp only [mem_univ, forall_true_left]
-  intro i
-  induction i using Ordinal.induction with
-  | h j ih =>
-    refine h j ?_
-    rw [LawfulBefore, lawfulIn_iff]
-    exact ih
-
-theorem mem_before_smul_iff_mem_before (A : ExtendedIndex β) (i : Ordinal)
-    (P : InflexibleCoePath A) (ih : LawfulBefore hσS hσT hS hT i)
-    (c : SupportCondition P.δ) :
-    c ∈ (S.before i).comp P.δ (P.B.cons (coe_lt P.hδ)) ↔
-    Tree.comp (P.B.cons (coe_lt P.hδ))
-        (Allowable.toStructPerm (convertAllowable hσS hσT hS hT)) • c ∈
-      ((T.before i).comp P.δ (P.B.cons (coe_lt P.hδ))) := by
-  constructor
-  · rintro ⟨h₁, h₂⟩
-    refine ⟨ih.smul_mem ⟨_, h₁⟩ h₂, ?_⟩
-    change typein T.r ⟨convertAllowable hσS hσT hS hT •
-      ⟨(P.B.cons (coe_lt P.hδ)).comp c.path, c.value⟩, _⟩ < _
-    rw [ih.typein_smul ⟨_, h₁⟩ h₂]
-    exact h₂
-  · rintro ⟨h₁, h₂⟩
-    change convertAllowable hσS hσT hS hT •
-      ⟨(P.B.cons (coe_lt P.hδ)).comp c.path, c.value⟩ ∈ T at h₁
-    change typein T.r ⟨(convertAllowable hσS hσT hS hT •
-      ⟨(P.B.cons (coe_lt P.hδ)).comp c.path, c.value⟩), _⟩ < _ at h₂
-    refine ⟨?_, ?_⟩
-    · have := ih.inv_smul_mem ⟨_, h₁⟩ h₂
-      rw [inv_smul_smul] at this
-      exact this
-    · simp only [← ih.typein_inv_smul ⟨_, h₁⟩ h₂, inv_smul_smul] at h₂
-      exact h₂
-
-theorem before_smul_eq_before (A : ExtendedIndex β) (i : Ordinal)
-    (P : InflexibleCoePath A) (ih : LawfulBefore hσS hσT hS hT i) :
-    (S.before i).comp P.δ (P.B.cons (coe_lt P.hδ)) =
-    (show Allowable (P.δ : Iic α) from
-      (Allowable.comp (show Path ((β : IicBot α) : TypeIndex) (P.δ : IicBot α) from
-          P.B.cons (coe_lt P.hδ)))
-        (convertAllowable hσS hσT hS hT))⁻¹ •
-    (T.before i).comp P.δ (P.B.cons (coe_lt P.hδ)) := by
-  dsimp only
-  refine OrdSupport.ext ?_ ?_ ?_
-  · intro c
-    rw [mem_before_smul_iff_mem_before hσS hσT hS hT A i P ih c,
-      OrdSupport.smul_mem, inv_inv, Allowable.smul_supportCondition,
-      Allowable.toStructPerm_comp (show Path ((β : IicBot α) : TypeIndex) (P.δ : IicBot α) from
-        P.B.cons (coe_lt P.hδ))]
-    exact id
-  · intro c
-    rw [mem_before_smul_iff_mem_before hσS hσT hS hT A i P ih c,
-      OrdSupport.smul_mem, inv_inv, Allowable.smul_supportCondition,
-      Allowable.toStructPerm_comp (show Path ((β : IicBot α) : TypeIndex) (P.δ : IicBot α) from
-        P.B.cons (coe_lt P.hδ))]
-    exact id
-  · intro c d
-    have hc := ih.smul_eq ⟨_, c.prop.1⟩ c.prop.2
-    have hd := ih.smul_eq ⟨_, d.prop.1⟩ d.prop.2
-    simp only [Allowable.smul_supportCondition, SupportCondition.ext_iff] at hc hd
-    have := Allowable.toStructPerm_comp
-      (show Path ((β : IicBot α) : TypeIndex) (P.δ : IicBot α) from P.B.cons (coe_lt P.hδ))
-      (convertAllowable hσS hσT hS hT)
-    dsimp only at this
-    simp only [OrdSupport.comp_lt, OrdSupport.before_lt, OrdSupport.lt_iff_smul, inv_inv,
-      Allowable.smul_supportCondition, this, Tree.comp_apply, hc.2, hd.2,
-      convertCondition_mk hσS hσT hS hT ((P.B.cons (coe_lt P.hδ)).comp c.val.path),
-      convertCondition_mk hσS hσT hS hT ((P.B.cons (coe_lt P.hδ)).comp d.val.path),
-      Subtype.coe_eta, convertCondition_lt]
-
-theorem spec_inflexibleBot (A : ExtendedIndex β) (L : Litter) (hL : InflexibleBot A L)
-    (haS : ⟨hL.path.B.cons (bot_lt_coe _), inl hL.a⟩ ∈ S) (hLS₁ : ⟨A, inr L.toNearLitter⟩ ∈ S)
-    (hLS₂ : σ.cond (typein S.r ⟨_, hLS₁⟩) (typein_lt hσS) =
-      SpecCondition.inflexibleBot A hL.path (typein S.r ⟨_, haS⟩)) :
-    ∃ hL' : InflexibleBot A (convertLitter hσS hσT hT A L hLS₁),
-    ∃ haT : ⟨hL'.path.B.cons (bot_lt_coe _), inl hL'.a⟩ ∈ T,
-      hL.path = hL'.path ∧ typein S.r ⟨_, haS⟩ = typein T.r ⟨_, haT⟩ := by
-  obtain (hL' | ⟨⟨hL'⟩⟩ | ⟨⟨hL'⟩⟩) := flexible_cases' β A (convertLitter hσS hσT hT A L hLS₁)
-  · have := hσT.flexible_spec A
-      (convertLitter hσS hσT hT A L hLS₁).toNearLitter
-      (convertLitter_mem hσS hσT hT A L hLS₁) hL'
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter] at this
-    rw [hLS₂] at this
-    cases this
-  · obtain ⟨_, this⟩ := hσT.inflexibleBot_spec A
-      (convertLitter hσS hσT hT A L hLS₁).toNearLitter
-      (convertLitter_mem hσS hσT hT A L hLS₁) hL'
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter] at this
-    rw [hLS₂] at this
-    exact ⟨hL', _, SpecCondition.inflexibleBot_injective this⟩
-  · obtain ⟨_, _, _, _, this⟩ := hσT.inflexibleCoe_spec A
-      (convertLitter hσS hσT hT A L hLS₁).toNearLitter
-      (convertLitter_mem hσS hσT hT A L hLS₁) hL'
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter] at this
-    rw [hLS₂] at this
-    cases this
-
-theorem spec_inflexibleBot_inv (A : ExtendedIndex β) (L : Litter) (hL : InflexibleBot A L)
-    (haT : ⟨hL.path.B.cons (bot_lt_coe _), inl hL.a⟩ ∈ T) (hLT₁ : ⟨A, inr L.toNearLitter⟩ ∈ T)
-    (hLT₂ : σ.cond (typein T.r ⟨_, hLT₁⟩) (typein_lt hσT) =
-      SpecCondition.inflexibleBot A hL.path (typein T.r ⟨_, haT⟩)) :
-    ∃ hL' : InflexibleBot A (convertLitter hσT hσS hS A L hLT₁),
-    ∃ haS : ⟨hL'.path.B.cons (bot_lt_coe _), inl hL'.a⟩ ∈ S,
-      hL.path = hL'.path ∧ typein T.r ⟨_, haT⟩ = typein S.r ⟨_, haS⟩ := by
-  obtain (hL' | ⟨⟨hL'⟩⟩ | ⟨⟨hL'⟩⟩) := flexible_cases' β A (convertLitter hσT hσS hS A L hLT₁)
-  · have := hσS.flexible_spec A
-      (convertLitter hσT hσS hS A L hLT₁).toNearLitter
-      (convertLitter_mem hσT hσS hS A L hLT₁) hL'
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter] at this
-    rw [hLT₂] at this
-    cases this
-  · obtain ⟨_, this⟩ := hσS.inflexibleBot_spec A
-      (convertLitter hσT hσS hS A L hLT₁).toNearLitter
-      (convertLitter_mem hσT hσS hS A L hLT₁) hL'
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter] at this
-    rw [hLT₂] at this
-    exact ⟨hL', _, SpecCondition.inflexibleBot_injective this⟩
-  · obtain ⟨_, _, _, _, this⟩ := hσS.inflexibleCoe_spec A
-      (convertLitter hσT hσS hS A L hLT₁).toNearLitter
-      (convertLitter_mem hσT hσS hS A L hLT₁) hL'
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter] at this
-    rw [hLT₂] at this
-    cases this
-
-theorem spec_inflexibleCoe (A : ExtendedIndex β) (L : Litter) (hL : InflexibleCoe A L)
-    (χ : CodingFunction hL.path.δ) (hχ : χ.Strong)
-    (hLS₁ : ⟨A, inr L.toNearLitter⟩ ∈ S)
-    (hLS₂ : σ.cond (typein S.r ⟨_, hLS₁⟩) (typein_lt hσS) =
-      SpecCondition.inflexibleCoe A hL.path χ hχ) :
-    ∃ hL' : InflexibleCoe A (convertLitter hσS hσT hT A L hLS₁),
-    ∃ hχT : (T.before (typein S.r ⟨_, hLS₁⟩)).comp hL.path.δ (hL.path.B.cons hL.path.hδ) ∈ χ,
-    hL.path = hL'.path ∧ HEq ((χ.decode _).get hχT) hL'.t := by
-  obtain (hL' | ⟨⟨hL'⟩⟩ | ⟨⟨hL'⟩⟩) := flexible_cases' β A (convertLitter hσS hσT hT A L hLS₁)
-  · have := hσT.flexible_spec A
-      (convertLitter hσS hσT hT A L hLS₁).toNearLitter
-      (convertLitter_mem hσS hσT hT A L hLS₁) hL'
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter] at this
-    rw [hLS₂] at this
-    cases this
-  · obtain ⟨_, this⟩ := hσT.inflexibleBot_spec A
-      (convertLitter hσS hσT hT A L hLS₁).toNearLitter
-      (convertLitter_mem hσS hσT hT A L hLS₁) hL'
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter] at this
-    rw [hLS₂] at this
-    cases this
-  · obtain ⟨χ, hχ₁, hχ₂, hχ₃, this⟩ := hσT.inflexibleCoe_spec A
-      (convertLitter hσS hσT hT A L hLS₁).toNearLitter
-      (convertLitter_mem hσS hσT hT A L hLS₁) hL'
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter] at this
-    rw [hLS₂] at this
-    refine ⟨hL', ?_⟩
-    obtain ⟨P, t, hL⟩ := hL
-    obtain ⟨P', t', hL'⟩ := hL'
-    cases SpecCondition.inflexibleCoe_injective₁ this
-    cases SpecCondition.inflexibleCoe_injective₂ this
-    simp only [Litter.toNearLitter_fst, OrdSupport.coe_sort_coe, typein_convertLitter] at hχ₂ hχ₃
-    exact ⟨hχ₂, rfl, heq_of_eq hχ₃⟩
-
-theorem spec_inflexibleCoe_inv (A : ExtendedIndex β) (L : Litter) (hL : InflexibleCoe A L)
-    (χ : CodingFunction hL.path.δ) (hχ : χ.Strong)
-    (hLT₁ : ⟨A, inr L.toNearLitter⟩ ∈ T)
-    (hLT₂ : σ.cond (typein T.r ⟨_, hLT₁⟩) (typein_lt hσT) =
-      SpecCondition.inflexibleCoe A hL.path χ hχ) :
-    ∃ hL' : InflexibleCoe A (convertLitter hσT hσS hS A L hLT₁),
-    ∃ hχS : (S.before (typein T.r ⟨_, hLT₁⟩)).comp hL.path.δ (hL.path.B.cons hL.path.hδ) ∈ χ,
-    hL.path = hL'.path ∧ HEq ((χ.decode _).get hχS) hL'.t := by
-  obtain (hL' | ⟨⟨hL'⟩⟩ | ⟨⟨hL'⟩⟩) := flexible_cases' β A (convertLitter hσT hσS hS A L hLT₁)
-  · have := hσS.flexible_spec A
-      (convertLitter hσT hσS hS A L hLT₁).toNearLitter
-      (convertLitter_mem hσT hσS hS A L hLT₁) hL'
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter] at this
-    rw [hLT₂] at this
-    cases this
-  · obtain ⟨_, this⟩ := hσS.inflexibleBot_spec A
-      (convertLitter hσT hσS hS A L hLT₁).toNearLitter
-      (convertLitter_mem hσT hσS hS A L hLT₁) hL'
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter] at this
-    rw [hLT₂] at this
-    cases this
-  · obtain ⟨χ, hχ₁, hχ₂, hχ₃, this⟩ := hσS.inflexibleCoe_spec A
-      (convertLitter hσT hσS hS A L hLT₁).toNearLitter
-      (convertLitter_mem hσT hσS hS A L hLT₁) hL'
-    simp only [OrdSupport.coe_sort_coe, typein_convertLitter] at this
-    rw [hLT₂] at this
-    refine ⟨hL', ?_⟩
-    obtain ⟨P, t, hL⟩ := hL
-    obtain ⟨P', t', hL'⟩ := hL'
-    cases SpecCondition.inflexibleCoe_injective₁ this
-    cases SpecCondition.inflexibleCoe_injective₂ this
-    simp only [Litter.toNearLitter_fst, OrdSupport.coe_sort_coe, typein_convertLitter] at hχ₂ hχ₃
-    exact ⟨hχ₂, rfl, heq_of_eq hχ₃⟩
-
-theorem convert_inflexibleBot (A : ExtendedIndex β) (L : Litter) (hL : InflexibleBot A L)
-    (haS : ⟨(hL.path.B.cons (bot_lt_coe _)), inl hL.a⟩ ∈ S)
-    (hLS : ⟨((hL.path.B.cons (coe_lt hL.path.hε)).cons (bot_lt_coe _)),
-      inr (fuzz (show ((⊥ : IioBot α) : TypeIndex) ≠ (hL.path.ε : Λ) from bot_ne_coe)
-        hL.a).toNearLitter⟩ ∈ S) :
-    fuzz (show ((⊥ : IioBot α) : TypeIndex) ≠ (hL.path.ε : Λ) from bot_ne_coe)
-      (convertAtom hσS hσT hS hT (hL.path.B.cons (bot_lt_coe _)) hL.a haS) =
-    convertLitter hσS hσT hT ((hL.path.B.cons (coe_lt hL.path.hε)).cons (bot_lt_coe _))
-        (fuzz (show ((⊥ : IioBot α) : TypeIndex) ≠ (hL.path.ε : Λ) from bot_ne_coe) hL.a) hLS := by
-  simp_rw [← hL.hL, ← hL.path.hA] at hLS
-  have := hσS.inflexibleBot_spec A L.toNearLitter hLS hL
-  obtain ⟨h₁, h₂⟩ := this
-  obtain ⟨hL', ha', h₁', h₂'⟩ := spec_inflexibleBot hσS hσT hT A L hL haS hLS h₂
-  obtain ⟨P, a, hL⟩ := hL
-  obtain ⟨P', a', hL'⟩ := hL'
-  dsimp only at *
-  subst h₁'
-  cases convertAtom_eq_of_typein_eq hσS hσT hS hT h₂'
-  have := hL'
-  simp_rw [P.hA, hL] at this
-  rw [this]
-
-theorem convert_inflexibleCoe (A : ExtendedIndex β) (L : Litter) (hL : InflexibleCoe A L)
-    (hLS : ⟨((hL.path.B.cons (coe_lt hL.path.hε)).cons (bot_lt_coe _)),
-      inr (fuzz (coe_ne_coe.mpr <| coe_ne' hL.path.hδε) hL.t).toNearLitter⟩ ∈ S)
-    (ih : LawfulBefore hσS hσT hS hT (typein S.r ⟨_, hLS⟩)) :
-    fuzz (coe_ne_coe.mpr <| coe_ne' hL.path.hδε)
-      (Allowable.comp
-        (show Path ((β : IicBot α) : TypeIndex) (hL.path.δ : IicBot α) from
-          hL.path.B.cons (coe_lt hL.path.hδ))
-        (convertAllowable hσS hσT hS hT) • hL.t) =
-    convertLitter hσS hσT hT ((hL.path.B.cons (coe_lt hL.path.hε)).cons (bot_lt_coe _))
-      (fuzz (coe_ne_coe.mpr <| coe_ne' hL.path.hδε) hL.t) hLS := by
-  simp_rw [← hL.hL, ← hL.path.hA] at hLS ih
-  obtain ⟨χ, hχ₁, hχ₂, hχ₃, h⟩ := hσS.inflexibleCoe_spec A L.toNearLitter hLS hL
-  obtain ⟨hL', hχT, h₁, h₂⟩ := spec_inflexibleCoe hσS hσT hT A L hL χ hχ₁ hLS h
-  obtain ⟨P, t, hL⟩ := hL
-  obtain ⟨P', t', hL'⟩ := hL'
-  subst h₁
-  cases eq_of_heq h₂
-  clear h₂
-  dsimp only at *
-  simp_rw [hL, P.hA] at hL'
-  rw [hL']
-  refine congr_arg _ ?_
-  have := CodingFunction.decode_smul' _ _
-    (Allowable.comp
-      (show Path ((β : IicBot α) : TypeIndex) (P.δ : IicBot α) from
-        P.B.cons (coe_lt P.hδ))
-      (convertAllowable hσS hσT hS hT)⁻¹) hχT (CodingFunction.smul_mem _ hχT)
-  rw [← inv_smul_eq_iff] at this
-  refine Eq.trans ?_ this
-  clear this
-  simp only [map_inv, inv_inv, smul_left_cancel_iff]
-  refine Eq.trans hχ₃.symm (CodingFunction.decode_congr ?_)
-  exact before_smul_eq_before hσS hσT hS hT A _ P ih
-
-theorem convert_inflexibleCoe_inv (A : ExtendedIndex β) (L : Litter) (hL : InflexibleCoe A L)
-    (hLT : ⟨((hL.path.B.cons (coe_lt hL.path.hε)).cons (bot_lt_coe _)),
-      inr (fuzz (coe_ne_coe.mpr <| coe_ne' hL.path.hδε) hL.t).toNearLitter⟩ ∈ T)
-    (ih : LawfulBefore hσS hσT hS hT (typein T.r ⟨_, hLT⟩)) :
-    fuzz (coe_ne_coe.mpr <| coe_ne' hL.path.hδε)
-      (Allowable.comp
-        (show Path ((β : IicBot α) : TypeIndex) (hL.path.δ : IicBot α) from
-          hL.path.B.cons (coe_lt hL.path.hδ))
-        (convertAllowable hσS hσT hS hT)⁻¹ • hL.t) =
-    convertLitter hσT hσS hS ((hL.path.B.cons (coe_lt hL.path.hε)).cons (bot_lt_coe _))
-      (fuzz (coe_ne_coe.mpr <| coe_ne' hL.path.hδε) hL.t) hLT := by
-  simp_rw [← hL.hL, ← hL.path.hA] at hLT ih
-  obtain ⟨χ, hχ₁, hχ₂, hχ₃, h⟩ := hσT.inflexibleCoe_spec A L.toNearLitter hLT hL
-  obtain ⟨hL', hχT, h₁, h₂⟩ := spec_inflexibleCoe hσT hσS hS A L hL χ hχ₁ hLT h
-  obtain ⟨P, t, hL⟩ := hL
-  obtain ⟨P', t', hL'⟩ := hL'
-  subst h₁
-  cases eq_of_heq h₂
-  clear h₂
-  dsimp only at *
-  simp_rw [hL, P.hA] at hL'
-  rw [hL']
-  refine congr_arg _ ?_
-  have := CodingFunction.decode_smul' _ _
-    (Allowable.comp
-      (show Path ((β : IicBot α) : TypeIndex) (P.δ : IicBot α) from
-        P.B.cons (coe_lt P.hδ))
-      (convertAllowable hσS hσT hS hT)) hχT (CodingFunction.smul_mem _ hχT)
-  rw [← inv_smul_eq_iff] at this
-  refine Eq.trans ?_ this
-  clear this
-  simp only [map_inv, inv_inv, smul_left_cancel_iff]
-  refine Eq.trans hχ₃.symm (CodingFunction.decode_congr ?_)
-  have := before_smul_eq_before hσS hσT hS hT A _ P ih
-  rw [this]
-  simp only [OrdSupport.coe_sort_coe]
-  -- TODO: Tidy this up
-  have := @smul_inv_smul _ _ _ ?_ (Allowable.comp
-      (show Path ((β : IicBot α) : TypeIndex) (P.δ : IicBot α) from
-        P.B.cons (coe_lt P.hδ))
-      (convertAllowable hσS hσT hS hT))
-    (((T.before (typein T.r ⟨_, hLT⟩)).comp P.δ (P.B.cons (coe_lt P.hδ))))
-  swap
-  · show MulAction (Allowable (P.δ : Iic α)) (OrdSupport _)
-    infer_instance
-  simp_rw [← hL, ← P.hA] at this
-  convert this.symm
-
-theorem smul_atom_eq (A : ExtendedIndex β) (a : Atom) (hc : ⟨A, inl a⟩ ∈ S) :
-    Allowable.toStructPerm (convertAllowable hσS hσT hS hT) A • a =
-    convertAtom hσS hσT hS hT A a hc := by
-  rw [← (convertAllowable_spec hσS hσT hS hT A).map_atom a, StructAction.rc_smul_atom_eq]
-  rfl
-  exact Or.inl (Or.inl (Or.inl (Or.inl hc)))
-
-theorem inv_smul_atom_eq (A : ExtendedIndex β) (a : Atom) (hc : ⟨A, inl a⟩ ∈ T) :
-    (Allowable.toStructPerm (convertAllowable hσS hσT hS hT) A)⁻¹ • a =
-    convertAtom hσT hσS hT hS A a hc :=
-  by rw [inv_smul_eq_iff, smul_atom_eq hσS hσT hS hT A, convertAtom_convertAtom]
-
-theorem smul_litter_eq_of_lawfulBefore' (A : ExtendedIndex β) (L : Litter)
-    (hc : ⟨A, inr L.toNearLitter⟩ ∈ S) (ih : LawfulBefore hσS hσT hS hT (typein S.r ⟨_, hc⟩)) :
-    Allowable.toStructPerm (convertAllowable hσS hσT hS hT) A • L =
-    convertLitter hσS hσT hT A L hc := by
-  obtain (hL | ⟨⟨hL⟩⟩ | ⟨⟨hL⟩⟩) := flexible_cases' β A L
-  · rw [← (convertAllowable_spec hσS hσT hS hT A).map_litter L (Or.inl (Or.inl ⟨hc, hL⟩)),
-      StructAction.rc_smul_litter_eq,
-      NearLitterAction.flexibleLitterLocalPerm_apply_eq _ hc hL,
-      NearLitterAction.roughLitterMapOrElse_of_dom]
-    rfl
-  · simp_rw [hL.hL, hL.path.hA]
-    have ha : ⟨hL.path.B.cons _, inl hL.a⟩ ∈ S
-    · simp_rw [hL.hL, hL.path.hA] at hc
-      exact hS.transConstrains_mem _ ⟨_, hc⟩ (Reduced.mkAtom _)
-        (Relation.TransGen.single <| Constrains.fuzz_bot hL.path.hε hL.path.B hL.a)
-    rw [toStructPerm_smul_fuzz β hL.path.γ ⊥ hL.path.ε]
-    swap
-    · exact bot_lt_coe _
-    swap
-    · intro h
-      simp only [IioBot.bot_ne_mk_coe] at h
-    rw [← convert_inflexibleBot hσS hσT hS hT A L hL ha]
-    have := ih.smul_eq ⟨_, ha⟩ ?_
-    · rw [convertCondition_eq_convertAtom hσS hσT hS hT, Allowable.smul_supportCondition] at this
-      simp only [smul_inl, SupportCondition.mk.injEq, inl.injEq, true_and] at this
-      rw [← this, ← Allowable.comp_bot (show Path ((β : IicBot α) : TypeIndex) (⊥ : IicBot α) from
-          hL.path.B.cons (bot_lt_coe _))]
-      rfl
-    · simp only [OrdSupport.coe_sort_coe, mem_setOf_eq, typein_lt_typein, hL.hL, hL.path.hA]
-      exact hS.lt_of_transConstrains _ _
-        (Relation.TransGen.single (Constrains.fuzz_bot hL.path.hε hL.path.B hL.a))
-  · simp_rw [hL.hL, hL.path.hA]
-    rw [toStructPerm_smul_fuzz β hL.path.γ hL.path.δ hL.path.ε]
-    swap
-    · exact coe_lt_coe.mpr hL.path.hδ
-    swap
-    · intro h
-      simp only [Subtype.mk.injEq, coe_inj] at h
-      exact coe_ne' hL.path.hδε h
-    simp_rw [hL.hL, hL.path.hA] at hc ih
-    exact convert_inflexibleCoe hσS hσT hS hT A L hL hc ih
-
-theorem smul_litter_eq_of_lawfulBefore (A : ExtendedIndex β) (L : Litter)
-    (hc : ⟨A, inr L.toNearLitter⟩ ∈ S) (ih : LawfulBefore hσS hσT hS hT (typein S.r ⟨_, hc⟩)) :
-    Allowable.toStructPerm (convertAllowable hσS hσT hS hT) A • L.toNearLitter =
-    (convertLitter hσS hσT hT A L hc).toNearLitter :=
-  StructAction.smul_toNearLitter_eq_of_precise _ StructAction.refine_precise
-    (convertAllowable_spec hσS hσT hS hT) hc
-    (smul_litter_eq_of_lawfulBefore' hσS hσT hS hT A L hc ih)
-
-theorem inv_smul_litter_eq_of_lawfulBefore' (A : ExtendedIndex β) (L : Litter)
-    (hc : ⟨A, inr L.toNearLitter⟩ ∈ T) (ih : LawfulBefore hσS hσT hS hT (typein T.r ⟨_, hc⟩)) :
-    (Allowable.toStructPerm (convertAllowable hσS hσT hS hT) A)⁻¹ • L =
-    convertLitter hσT hσS hS A L hc := by
-  obtain (hL | ⟨⟨hL⟩⟩ | ⟨⟨hL⟩⟩) := flexible_cases' β A L
-  · rw [inv_smul_eq_iff,
-        ← (convertAllowable_spec hσS hσT hS hT A).map_litter _ (Or.inl (Or.inl ?_)),
-        StructAction.rc_smul_litter_eq,
-        NearLitterAction.flexibleLitterLocalPerm_apply_eq,
-        NearLitterAction.roughLitterMapOrElse_of_dom]
-    · simp only [StructAction.refine_apply, NearLitterAction.refine_litterMap, convert_litterMap,
-        convertLitter_convertLitter, Litter.toNearLitter_fst]
-    · exact convertLitter_mem hσT hσS hS A L _
-    · exact convertLitter_mem hσT hσS hS A L _
-    · exact convert_mapFlexible hσT hσS hT hS A L _ hL
-    · exact ⟨convertLitter_mem hσT hσS hS A L _, convert_mapFlexible hσT hσS hT hS A L _ hL⟩
-  · simp_rw [hL.hL, hL.path.hA]
-    have ha : ⟨hL.path.B.cons _, inl hL.a⟩ ∈ T
-    · simp_rw [hL.hL, hL.path.hA] at hc
-      exact hT.transConstrains_mem _ ⟨_, hc⟩ (Reduced.mkAtom _)
-        (Relation.TransGen.single <| Constrains.fuzz_bot hL.path.hε hL.path.B hL.a)
-    rw [← Tree.inv_apply, ← map_inv]
-    rw [toStructPerm_smul_fuzz β hL.path.γ ⊥ hL.path.ε]
-    swap
-    · exact bot_lt_coe _
-    swap
-    · intro h
-      simp only [IioBot.bot_ne_mk_coe] at h
-    rw [← convert_inflexibleBot hσT hσS hT hS A L hL ha]
-    have := ih.inv_smul_eq ⟨_, ha⟩ ?_
-    · rw [inv_smul_eq_iff,
-        convertCondition_eq_convertAtom hσT hσS hT hS, Allowable.smul_supportCondition] at this
-      simp only [smul_inl, SupportCondition.mk.injEq, inl.injEq, true_and] at this
-      rw [← inv_smul_eq_iff] at this
-      rw [← this, ← Allowable.comp_bot (show Path ((β : IicBot α) : TypeIndex) (⊥ : IicBot α) from
-          hL.path.B.cons (bot_lt_coe _)), map_inv]
-      rfl
-    · simp only [OrdSupport.coe_sort_coe, mem_setOf_eq, typein_lt_typein, hL.hL, hL.path.hA]
-      exact hT.lt_of_transConstrains _ _
-        (Relation.TransGen.single <| Constrains.fuzz_bot hL.path.hε hL.path.B hL.a)
-  · simp_rw [hL.hL, hL.path.hA]
-    rw [← Tree.inv_apply, ← map_inv]
-    rw [toStructPerm_smul_fuzz β hL.path.γ hL.path.δ hL.path.ε]
-    swap
-    · exact coe_lt_coe.mpr hL.path.hδ
-    swap
-    · intro h
-      simp only [Subtype.mk.injEq, coe_inj] at h
-      exact coe_ne' hL.path.hδε h
-    simp_rw [hL.hL, hL.path.hA] at hc ih
-    exact convert_inflexibleCoe_inv hσS hσT hS hT A L hL hc ih
-
-theorem inv_smul_litter_eq_of_lawfulBefore (A : ExtendedIndex β) (L : Litter)
-    (hc : ⟨A, inr L.toNearLitter⟩ ∈ T) (ih : LawfulBefore hσS hσT hS hT (typein T.r ⟨_, hc⟩)) :
-    (Allowable.toStructPerm (convertAllowable hσS hσT hS hT) A)⁻¹ • L.toNearLitter =
-    (convertLitter hσT hσS hS A L hc).toNearLitter := by
-  have := inv_smul_litter_eq_of_lawfulBefore' hσS hσT hS hT A L hc ih
-  rw [inv_smul_eq_iff] at this ⊢
-  rw [StructAction.smul_toNearLitter_eq_of_precise _ StructAction.refine_precise
-      (convertAllowable_spec hσS hσT hS hT) ?_
-      (this.symm.trans ?_)]
-  · simp only [StructAction.refine_apply, NearLitterAction.refine_litterMap, convert_litterMap,
-    convertLitter_convertLitter]
-  · exact convertLitter_mem hσT hσS hS _ _ _
-  · simp only [StructAction.refine_apply, NearLitterAction.refine_litterMap, convert_litterMap,
-    convertLitter_convertLitter, Litter.toNearLitter_fst]
-
-theorem lawfulIn_step (i : Ordinal) (ih : LawfulBefore hσS hσT hS hT i) :
-    LawfulIn hσS hσT hS hT {i} := by
-  constructor
-  case smul_eq =>
-    rintro ⟨⟨A, a | N⟩, hc⟩ rfl
-    · simp_rw [convertCondition_eq_convertAtom hσS hσT hS hT, ← smul_atom_eq hσS hσT hS hT A a hc]
-      rfl
-    · obtain ⟨L, rfl⟩ := (isLitter_of_reduced (hS.reduced_of_mem ⟨_, hc⟩)).exists_litter_eq
-      simp_rw [convertCondition_eq_convertLitter hσS hσT hT,
-        ← smul_litter_eq_of_lawfulBefore hσS hσT hS hT A L hc ih]
-      rfl
-  case inv_smul_eq =>
-    rintro ⟨⟨A, a | N⟩, hc⟩ rfl
-    · simp_rw [convertCondition_eq_convertAtom hσT hσS hT hS,
-        ← inv_smul_atom_eq hσS hσT hS hT A a hc]
-      simp only [Allowable.smul_supportCondition, smul_inl, map_inv, Tree.inv_apply]
-    · obtain ⟨L, rfl⟩ := (isLitter_of_reduced (hT.reduced_of_mem ⟨_, hc⟩)).exists_litter_eq
-      simp_rw [convertCondition_eq_convertLitter hσT hσS hS,
-        ← inv_smul_litter_eq_of_lawfulBefore hσS hσT hS hT A L hc ih]
-      simp only [Allowable.smul_supportCondition, smul_inr, map_inv, Tree.inv_apply]
-
-theorem lawfulIn_all : LawfulIn hσS hσT hS hT univ :=
-  lawfulBefore_induction hσS hσT hS hT (lawfulIn_step hσS hσT hS hT)
-
-theorem convertAllowable_smul : convertAllowable hσS hσT hS hT • S = T := by
-  refine OrdSupport.ext ?_ ?_ ?_
-  · intro c hc
-    have := (lawfulIn_all hσS hσT hS hT).smul_mem ⟨_, hc⟩ (mem_univ _)
-    rw [smul_inv_smul] at this
-    exact this
-  · intro c hc
-    exact (lawfulIn_all hσS hσT hS hT).inv_smul_mem ⟨_, hc⟩ (mem_univ _)
-  · intro c d
-    have hc := (lawfulIn_all hσS hσT hS hT).smul_eq ⟨_, c.prop⟩ (mem_univ _)
-    have hd := (lawfulIn_all hσS hσT hS hT).smul_eq ⟨_, d.prop⟩ (mem_univ _)
-    simp only [smul_inv_smul] at hc hd
-    conv_rhs => simp (config := { singlePass := true }) only [hc, hd]
-    simp only [OrdSupport.lt_iff_smul, Subtype.coe_eta, convertCondition_lt]
-
-end Spec
-
-end ConNF