diff --git a/ConNF/BaseType/Params.lean b/ConNF/BaseType/Params.lean
index d18cd80595..bc1d0a18b2 100644
--- a/ConNF/BaseType/Params.lean
+++ b/ConNF/BaseType/Params.lean
@@ -54,9 +54,10 @@ class Params where
   [κ_isWellOrder : IsWellOrder κ (· < ·)]
   κ_ord : Ordinal.type ((· < ·) : κ → κ → Prop) = (#κ).ord
   κ_isRegular : (#κ).IsRegular
+  [κ_succ : SuccOrder κ]
   [κ_addMonoid : AddMonoid κ]
-  [κ_covariant : CovariantClass κ κ (· + ·) (· ≤ ·)]
-  [κ_covariant_swap : CovariantClass κ κ (Function.swap (· + ·)) (· ≤ ·)]
+  κ_typein (i j : κ) : Ordinal.typein (· < ·) (i + j : κ) =
+    Ordinal.typein (· < ·) i + Ordinal.typein (· < ·) j
   Λ_lt_κ : #Λ < #κ
   /--
   A large type used in indexing the litters.
@@ -83,6 +84,41 @@ There exist valid parameters for the model. The smallest such parameters are
 * `μ = ℶ_{ω_1}`.
 -/
 
+theorem noMaxOrder_of_ordinal_type_eq {α : Type u} [Preorder α] [Infinite α] [IsWellOrder α (· < ·)]
+    (h : (Ordinal.type ((· < ·) : α → α → Prop)).IsLimit) : NoMaxOrder α := by
+  refine ⟨fun a => ?_⟩
+  have := (Ordinal.succ_lt_of_isLimit h).mpr (Ordinal.typein_lt_type (· < ·) a)
+  obtain ⟨b, hb⟩ := Ordinal.typein_surj (· < ·) this
+  refine ⟨b, ?_⟩
+  have := Order.lt_succ (Ordinal.typein (fun x y => x < y) a)
+  rw [← hb, Ordinal.typein_lt_typein] at this
+  exact this
+
+noncomputable def succOrderOfIsWellOrder {α : Type u} [Preorder α] [Infinite α]
+    [inst : IsWellOrder α (· < ·)] (h : (Ordinal.type ((· < ·) : α → α → Prop)).IsLimit) :
+    SuccOrder α where
+  succ := inst.toIsWellFounded.wf.succ
+  le_succ a := le_of_lt (WellFounded.lt_succ _ ((noMaxOrder_of_ordinal_type_eq h).exists_gt a))
+  max_of_succ_le ha hb :=
+    (ha.not_lt (WellFounded.lt_succ _ ((noMaxOrder_of_ordinal_type_eq h).exists_gt _))).elim
+  succ_le_of_lt := by
+    intro a b ha
+    by_contra hb
+    obtain hab | hab | hab :=
+      inst.toIsTrichotomous.trichotomous (inst.toIsWellFounded.wf.succ a) b
+    · exact hb hab.le
+    · exact hb hab.le
+    · rw [WellFounded.lt_succ_iff ((noMaxOrder_of_ordinal_type_eq h).exists_gt a)] at hab
+      obtain (hab | hab) := hab
+      exact ha.not_lt hab
+      exact ha.ne hab.symm
+  le_of_lt_succ := by
+    intro a b ha
+    rw [WellFounded.lt_succ_iff ((noMaxOrder_of_ordinal_type_eq h).exists_gt _)] at ha
+    obtain (ha | ha) := ha
+    exact ha.le
+    exact ha.le
+
 theorem typein_add_lt_of_type_eq_ord {α : Type _}
     [Infinite α] [LinearOrder α] [IsWellOrder α (· < ·)]
     (h : Ordinal.type ((· < ·) : α → α → Prop) = (#α).ord) (x y : α) :
@@ -162,33 +198,6 @@ noncomputable def addMonoid_of_type_eq_ord {α : Type _}
     simp only [Ordinal.typein_enum, Ordinal.enum_inj, add_assoc]
   __ := addZeroClass_of_type_eq_ord h
 
-noncomputable def add_covariant_of_type_eq_ord {α : Type _}
-    [Infinite α] [LinearOrder α] [IsWellOrder α (· < ·)]
-    (h : Ordinal.type ((· < ·) : α → α → Prop) = (#α).ord) :
-    CovariantClass α α (add_of_type_eq_ord h).add (· ≤ ·) where
-  elim x y z := by
-    contrapose
-    rw [not_le, not_le]
-    intro h
-    have := (Ordinal.enum_lt_enum _ _).mp h
-    simp only [add_lt_add_iff_left, Ordinal.typein_lt_typein] at this
-    exact this
-
-noncomputable def add_covariant_swap_of_type_eq_ord {α : Type _}
-    [Infinite α] [LinearOrder α] [IsWellOrder α (· < ·)]
-    (h : Ordinal.type ((· < ·) : α → α → Prop) = (#α).ord) :
-    CovariantClass α α (Function.swap (add_of_type_eq_ord h).add) (· ≤ ·) where
-  elim x y z := by
-    contrapose
-    rw [not_le, not_le]
-    intro h
-    have := (Ordinal.enum_lt_enum _ _).mp h
-    obtain (h' | h' | h') := lt_trichotomy z y
-    · exact h'
-    · subst h'
-      simp only [lt_self_iff_false] at this
-    · cases (add_le_add_right ((Ordinal.typein_lt_typein (· < ·)).mpr h').le _).not_lt this
-
 noncomputable example : Params.{0} where
   Λ := ℕ
   Λ_zero_le := zero_le
@@ -200,18 +209,15 @@ noncomputable example : Params.{0} where
   κ_isRegular := by
     simp only [Cardinal.card_ord, Cardinal.mk_ordinal_out]
     exact isRegular_aleph_one
-  κ_addMonoid :=
-    let _ : Infinite (aleph 1).ord.out.α :=
-      by simp only [Cardinal.infinite_iff, mk_ordinal_out, card_ord, aleph0_le_aleph]
-    addMonoid_of_type_eq_ord (by simp)
-  κ_covariant :=
+  κ_succ :=
     let _ : Infinite (aleph 1).ord.out.α :=
       by simp only [Cardinal.infinite_iff, mk_ordinal_out, card_ord, aleph0_le_aleph]
-    add_covariant_of_type_eq_ord (by simp)
-  κ_covariant_swap :=
+    succOrderOfIsWellOrder (by rw [Ordinal.type_lt]; exact ord_aleph_isLimit 1)
+  κ_addMonoid :=
     let _ : Infinite (aleph 1).ord.out.α :=
       by simp only [Cardinal.infinite_iff, mk_ordinal_out, card_ord, aleph0_le_aleph]
-    add_covariant_swap_of_type_eq_ord (by simp)
+    addMonoid_of_type_eq_ord (by simp)
+  κ_typein i j := Ordinal.typein_enum _ _
   Λ_lt_κ := by
     rw [mk_denumerable, mk_ordinal_out, card_ord]
     exact aleph0_lt_aleph_one
@@ -228,16 +234,6 @@ noncomputable example : Params.{0} where
     rw [beth_normal.cof_eq (ord_isLimit <| aleph0_le_aleph 1)]
     exact isRegular_aleph_one.2
 
-theorem noMaxOrder_of_ordinal_type_eq {α : Type u} [Preorder α] [Infinite α] [IsWellOrder α (· < ·)]
-    (h : (Ordinal.type ((· < ·) : α → α → Prop)).IsLimit) : NoMaxOrder α := by
-  refine ⟨fun a => ?_⟩
-  have := (Ordinal.succ_lt_of_isLimit h).mpr (Ordinal.typein_lt_type (· < ·) a)
-  obtain ⟨b, hb⟩ := Ordinal.typein_surj (· < ·) this
-  refine ⟨b, ?_⟩
-  have := Order.lt_succ (Ordinal.typein (fun x y => x < y) a)
-  rw [← hb, Ordinal.typein_lt_typein] at this
-  exact this
-
 variable [Params.{u}] {ι α β : Type u}
 
 /-! The types `Λ`, `κ`, `μ` are inhabited and infinite. -/
@@ -260,11 +256,14 @@ instance : NoMaxOrder Λ := noMaxOrder_of_ordinal_type_eq Params.Λ_isLimit
 
 instance : LinearOrder κ := Params.κ_linearOrder
 instance : IsWellOrder κ (· < ·) := Params.κ_isWellOrder
+instance : SuccOrder κ := Params.κ_succ
 instance : AddMonoid κ := Params.κ_addMonoid
-instance : CovariantClass κ κ (· + ·) (· ≤ ·) := Params.κ_covariant
-instance : CovariantClass κ κ (Function.swap (· + ·)) (· ≤ ·) := Params.κ_covariant_swap
 instance : Inhabited κ := ⟨0⟩
 instance : Infinite κ := Cardinal.infinite_iff.mpr Params.κ_isRegular.aleph0_le
+instance : NoMaxOrder κ := by
+  have := Cardinal.ord_isLimit Params.κ_isRegular.aleph0_le
+  rw [← Params.κ_ord] at this
+  exact noMaxOrder_of_ordinal_type_eq this
 
 instance : LinearOrder μ := Params.μ_linearOrder
 instance : IsWellOrder μ (· < ·) := Params.μ_isWellOrder
@@ -275,6 +274,74 @@ instance : NoMaxOrder μ := by
   rw [← Params.μ_ord] at this
   exact noMaxOrder_of_ordinal_type_eq this
 
+def κ_ofNat : ℕ → κ
+  | 0 => 0
+  | n + 1 => Order.succ (κ_ofNat n)
+
+instance (n : ℕ) : OfNat κ n := ⟨κ_ofNat n⟩
+
+instance : CovariantClass κ κ (· + ·) (· ≤ ·) := by
+  constructor
+  intro i j k h
+  rw [← not_lt, ← Ordinal.typein_le_typein (· < ·)] at h ⊢
+  rw [Params.κ_typein, Params.κ_typein]
+  exact add_le_add_left h _
+
+instance : CovariantClass κ κ (Function.swap (· + ·)) (· ≤ ·) := by
+  constructor
+  intro i j k h
+  rw [← not_lt, ← Ordinal.typein_le_typein (· < ·)] at h ⊢
+  rw [Params.κ_typein, Params.κ_typein]
+  exact add_le_add_right h _
+
+@[simp]
+theorem κ_typein_zero : Ordinal.typein ((· < ·) : κ → κ → Prop) 0 = 0 := by
+  have := add_zero (0 : κ)
+  rw [← Ordinal.typein_inj (· < ·), Params.κ_typein] at this
+  conv at this => rhs; rw [← add_zero (Ordinal.typein _ _)]
+  rw [Ordinal.add_left_cancel] at this
+  exact this
+
+theorem κ_le_zero_iff (i : κ) : i ≤ 0 ↔ i = 0 :=
+  by rw [← not_lt, ← Ordinal.typein_le_typein (· < ·), κ_typein_zero, Ordinal.le_zero,
+    ← κ_typein_zero, Ordinal.typein_inj]
+
+@[simp]
+theorem κ_add_eq_zero_iff (i j : κ) : i + j = 0 ↔ i = 0 ∧ j = 0 :=
+  by rw [← Ordinal.typein_inj (α := κ) (· < ·), ← Ordinal.typein_inj (α := κ) (· < ·),
+    ← Ordinal.typein_inj (α := κ) (· < ·), Params.κ_typein, κ_typein_zero, Ordinal.add_eq_zero_iff]
+
+@[simp]
+theorem κ_succ_typein (i : κ) :
+    Ordinal.typein ((· < ·) : κ → κ → Prop) (Order.succ i) =
+    Ordinal.typein ((· < ·) : κ → κ → Prop) i + 1 := by
+  refine le_antisymm ?_ ?_
+  · have : i < Ordinal.enum (· < ·) (Ordinal.typein ((· < ·) : κ → κ → Prop) i + 1) ?_
+    · conv_lhs => rw [← Ordinal.enum_typein ((· < ·) : κ → κ → Prop) i]
+      rw [Ordinal.enum_lt_enum (r := (· < ·))]
+      · exact lt_add_one _
+      · have := Order.lt_succ i
+        rw [← Ordinal.typein_lt_typein ((· < ·) : κ → κ → Prop)] at this
+        exact (Order.succ_le_of_lt this).trans_lt (Ordinal.typein_lt_type _ _)
+    have := Order.succ_le_of_lt this
+    conv at this => lhs; rw [← Ordinal.enum_typein ((· < ·) : κ → κ → Prop) (Order.succ i)]
+    rw [← not_lt, Ordinal.enum_le_enum] at this
+    exact this
+  · simp only [Ordinal.add_one_eq_succ, Order.succ_le_iff, Ordinal.typein_lt_typein,
+      Order.lt_succ_iff_not_isMax, gt_iff_lt, not_isMax, not_false_eq_true]
+
+theorem κ_zero_lt_one : (0 : κ) < 1 := by
+  rw [← Ordinal.typein_lt_typein ((· < ·) : κ → κ → Prop)]
+  exact lt_of_lt_of_eq (lt_add_one _) (κ_succ_typein 0).symm
+
+@[simp]
+theorem κ_lt_one_iff (i : κ) : i < 1 ↔ i = 0 := by
+  constructor
+  · rw [← κ_le_zero_iff]
+    exact SuccOrder.le_of_lt_succ
+  · rintro rfl
+    exact κ_zero_lt_one
+
 /-- Either the base type or a proper type index (an element of `Λ`).
 The base type is written `⊥`. -/
 @[reducible]
diff --git a/ConNF/FOA/Basic/Constrains.lean b/ConNF/FOA/Basic/Constrains.lean
index 3444543b29..be165c164a 100644
--- a/ConNF/FOA/Basic/Constrains.lean
+++ b/ConNF/FOA/Basic/Constrains.lean
@@ -405,9 +405,9 @@ theorem small_constrains {β : Λ} (c : SupportCondition β) : Small {d | d ≺
     · obtain ⟨γ, _, δ, _, ε, _, hδ, hε, hδε, B, t, rfl, rfl⟩ := h
       refine lt_of_le_of_lt ?_ (designatedSupport t).small
       suffices
-        #{a : SupportCondition β |
-            ∃ c : designatedSupport t, a = ⟨(B.cons hδ).comp c.val.path, c.val.value⟩} ≤
-          #(designatedSupport t) by
+        #{a : SupportCondition β | ∃ c : (designatedSupport t : Set (SupportCondition δ)),
+            a = ⟨(B.cons hδ).comp c.val.path, c.val.value⟩} ≤
+          #(designatedSupport t : Set (SupportCondition δ)) by
         refine le_trans (Cardinal.mk_subtype_le_of_subset ?_) this
         rintro x ⟨_, _, _, _, _, _, _, _, _, _, _, c, hc, rfl, h⟩
         rw [SupportCondition.mk.injEq] at h
diff --git a/ConNF/FOA/Basic/Reduction.lean b/ConNF/FOA/Basic/Reduction.lean
index 3a5ff2ac8f..fc7183a6f8 100644
--- a/ConNF/FOA/Basic/Reduction.lean
+++ b/ConNF/FOA/Basic/Reduction.lean
@@ -184,29 +184,8 @@ theorem reduction_supports (S : Set (SupportCondition β)) (c : SupportCondition
 theorem reduction_designatedSupport_supports [TangleData β] (t : Tangle β) :
     Supports (Allowable β) (reduction (designatedSupport t : Set (SupportCondition β))) t := by
   intro ρ h
-  refine (designatedSupport t).supports ρ ?_
+  refine designatedSupport_supports t ρ ?_
   intros c hc'
   exact reduction_supports (designatedSupport t) c hc' (Allowable.toStructPerm ρ) h
 
-/-- A support for a tangle containing only reduced support conditions. -/
-noncomputable def reducedSupport [TangleData β] (t : Tangle β) : Support β (Allowable β) t
-    where
-  carrier := reduction (designatedSupport t : Set (SupportCondition β))
-  small := reduction_small (designatedSupport t).small
-  supports := reduction_designatedSupport_supports t
-
-theorem mem_reducedSupport_iff [TangleData β] (t : Tangle β) (c : SupportCondition β) :
-    c ∈ reducedSupport t ↔ c ∈ reduction (designatedSupport t : Set (SupportCondition β)) :=
-  Iff.rfl
-
-theorem lt_of_mem_reducedSupport
-    {β γ δ ε : Λ} [LeLevel β] [LeLevel γ] [LtLevel δ] [LtLevel ε]
-    (hδ : (δ : TypeIndex) < γ) (hε : (ε : TypeIndex) < γ) (hδε : (δ : TypeIndex) ≠ ε)
-    (B : Path (β : TypeIndex) γ) (t : Tangle δ)
-    (c : SupportCondition δ) (h : c ∈ reducedSupport t) :
-    (⟨(B.cons hδ).comp c.path, c.value⟩ : SupportCondition β) <
-      ⟨(B.cons hε).cons (bot_lt_coe _), inr (fuzz hδε t).toNearLitter⟩ := by
-  obtain ⟨⟨d, hd, hcd⟩, _⟩ := h
-  exact Relation.TransGen.tail' (le_comp hcd _) (Constrains.fuzz hδ hε hδε B t d hd)
-
 end ConNF
diff --git a/ConNF/FOA/Properties/Injective.lean b/ConNF/FOA/Properties/Injective.lean
index 8673def5bb..5986bd452e 100644
--- a/ConNF/FOA/Properties/Injective.lean
+++ b/ConNF/FOA/Properties/Injective.lean
@@ -218,7 +218,7 @@ theorem Biexact.smul_eq_smul {β : Λ} [LeLevel β] {π π' : Allowable β} {c :
     refine h₁.trans (h₂.trans ?_).symm
     refine' congr_arg _ _
     rw [← inv_smul_eq_iff, smul_smul]
-    refine' (designatedSupport t).supports _ _
+    refine' designatedSupport_supports t _ _
     intro c hc
     rw [mul_smul, inv_smul_eq_iff]
     simp only [Allowable.toStructPerm_smul, Allowable.toStructPerm_comp, Tree.comp_comp]
@@ -423,7 +423,7 @@ theorem supports {β : Λ} [LeLevel β] {π π' : Allowable β} {t : Tangle β}
       Allowable.toStructPerm π' A • N) :
     π • t = π' • t := by
   rw [← inv_smul_eq_iff, smul_smul]
-  refine' (designatedSupport t).supports _ _
+  refine' designatedSupport_supports t _ _
   intro c hc
   rw [mul_smul, inv_smul_eq_iff]
   simp only [Allowable.smul_supportCondition_eq_smul_iff]
@@ -802,7 +802,7 @@ theorem ihAction_smul_tangle' (hπf : π.Free) (c d : SupportCondition β) (A :
         (ihsAction_comp_mapFlexible hπf _ _ _) • hL₂.t := by
   obtain ⟨⟨γ, δ, ε, hδ, hε, hδε, B, rfl⟩, t, rfl⟩ := hL₂
   rw [← inv_smul_eq_iff, smul_smul]
-  refine' (designatedSupport t).supports _ _
+  refine' designatedSupport_supports t _ _
   intro e he
   rw [mul_smul, inv_smul_eq_iff]
   simp only [ne_eq, Allowable.smul_supportCondition_eq_smul_iff]
diff --git a/ConNF/Fuzz/Hypotheses.lean b/ConNF/Fuzz/Hypotheses.lean
index f273477a63..d9249c33d4 100644
--- a/ConNF/Fuzz/Hypotheses.lean
+++ b/ConNF/Fuzz/Hypotheses.lean
@@ -41,10 +41,11 @@ class TangleData (α : TypeIndex) where
   [allowableGroup : Group Allowable]
   allowableToStructPerm : Allowable →* StructPerm α
   [allowableAction : MulAction Allowable Tangle]
-  designatedSupport :
+  designatedSupport : Tangle → Support α
+  designatedSupport_supports (t : Tangle) :
     haveI : MulAction Allowable (SupportCondition α) :=
       MulAction.compHom _ allowableToStructPerm
-    (t : Tangle) → Support α Allowable t
+    MulAction.Supports Allowable (designatedSupport t : Set (SupportCondition α)) t
 
 export TangleData (Tangle Allowable)
 
@@ -87,9 +88,13 @@ end Allowable
 
 /-- For each tangle, we provide a small support for it. This is known as the designated support of
 the tangle. -/
-def designatedSupport {α : TypeIndex} [TangleData α] (t : Tangle α) : Support α (Allowable α) t :=
+def designatedSupport {α : TypeIndex} [TangleData α] (t : Tangle α) : Support α :=
   TangleData.designatedSupport t
 
+theorem designatedSupport_supports {α : TypeIndex} [TangleData α] (t : Tangle α) :
+    MulAction.Supports (Allowable α) (designatedSupport t : Set (SupportCondition α)) t :=
+  TangleData.designatedSupport_supports t
+
 class PositionedTangles (α : TypeIndex) [TangleData α] where
   /-- A position function, giving each tangle a unique position `ν : μ`.
   The existence of this injection proves that there are at most `μ` tangles at level `α`.
@@ -140,14 +145,11 @@ instance Bot.tangleData : TangleData ⊥
   Allowable := NearLitterPerm
   allowableToStructPerm := Tree.toBotIso.toMonoidHom
   allowableAction := inferInstance
-  designatedSupport a :=
-    { carrier := {⟨Quiver.Path.nil, Sum.inl a⟩}
-      supports := fun π => by
-        intro h
-        simp only [mem_singleton_iff, NearLitterPerm.smul_supportCondition_eq_iff, forall_eq,
-          Sum.smul_inl, Sum.inl.injEq] at h
-        exact h
-      small := small_singleton _ }
+  designatedSupport a := ⟨1, fun _ _ => ⟨Quiver.Path.nil, Sum.inl a⟩⟩
+  designatedSupport_supports a π h := by
+    simp only [Support.mem_carrier_iff, κ_lt_one_iff, exists_prop, exists_eq_left,
+      NearLitterPerm.smul_supportCondition_eq_iff, forall_eq, Sum.smul_inl, Sum.inl.injEq] at h
+    exact h
 
 /-- A position function for atoms, which is chosen arbitrarily. -/
 noncomputable instance instPositionAtom : Position Atom μ :=
diff --git a/ConNF/NewTangle/NewTangle.lean b/ConNF/NewTangle/NewTangle.lean
index 780dbfe978..270feb3e09 100644
--- a/ConNF/NewTangle/NewTangle.lean
+++ b/ConNF/NewTangle/NewTangle.lean
@@ -400,7 +400,8 @@ end NewAllowable
 This is `τ_α` in the blueprint.
 Unlike the type `tangle`, this is not an opaque definition, and we can inspect and unfold it. -/
 def NewTangle :=
-  { t : Semitangle // Supported α NewAllowable t }
+  { t : Semitangle //
+    ∃ S : Support α, MulAction.Supports NewAllowable (S : Set (SupportCondition α)) t }
 
 variable {c d : Code} {S : Set (SupportCondition α)}
 
@@ -419,9 +420,11 @@ theorem Code.Equiv.supports_iff (hcd : c ≡ d) :
 
 /-- If two codes are equivalent, one is supported if and only if the other is. -/
 theorem Code.Equiv.supported_iff (hcd : c ≡ d) :
-    Supported α NewAllowable c ↔ Supported α NewAllowable d :=
-  ⟨fun ⟨⟨s, hs, h⟩⟩ => ⟨⟨s, hs, hcd.supports h⟩⟩,
-    fun ⟨⟨s, hs, h⟩⟩ => ⟨⟨s, hs, hcd.symm.supports h⟩⟩⟩
+    (∃ S : Support α, MulAction.Supports NewAllowable (S : Set (SupportCondition α)) c) ↔
+    ∃ S : Support α, MulAction.Supports NewAllowable (S : Set (SupportCondition α)) d := by
+  constructor <;> rintro ⟨S, hS⟩
+  · exact ⟨S, hcd.supports hS⟩
+  · exact ⟨S, hcd.symm.supports hS⟩
 
 @[simp]
 theorem smul_intro {β : TypeIndex} [inst : LtLevel β]  (ρ : NewAllowable) (s : Set (Tangle β)) (hs) :
@@ -457,17 +460,19 @@ theorem NewAllowable.smul_supportCondition_eq_smul_iff
 This is called a *typed near litter*. -/
 def newTypedNearLitter (N : NearLitter) : NewTangle :=
   ⟨intro (show Set (Tangle ⊥) from N.2.1) <| Code.isEven_bot _,
-    ⟨⟨{⟨Quiver.Hom.toPath (bot_lt_coe _), Sum.inr N⟩}, small_singleton _, fun ρ h => by
-        simp only [smul_intro]
-        congr 1
-        simp only [mem_singleton_iff, NewAllowable.smul_supportCondition_eq_iff, forall_eq,
-          Sum.smul_inr, Sum.inr.injEq] at h
-        apply_fun SetLike.coe at h
-        refine Eq.trans ?_ h
-        rw [NearLitterPerm.smul_nearLitter_coe]
-        change _ '' _ = _ '' _
-        simp_rw [SemiallowablePerm.coe_apply_bot]
-        rfl⟩⟩⟩
+    ⟨1, fun _ _ => ⟨Quiver.Hom.toPath (bot_lt_coe _), Sum.inr N⟩⟩,
+    by
+      intro ρ h
+      simp only [smul_intro]
+      congr 1
+      simp only [Support.mem_carrier_iff, κ_lt_one_iff, exists_prop, exists_eq_left,
+        NewAllowable.smul_supportCondition_eq_iff, forall_eq, Sum.smul_inr, Sum.inr.injEq] at h
+      apply_fun SetLike.coe at h
+      refine Eq.trans ?_ h
+      rw [NearLitterPerm.smul_nearLitter_coe]
+      change _ '' _ = _ '' _
+      simp_rw [SemiallowablePerm.coe_apply_bot]
+      rfl⟩
 
 namespace NewTangle
 
@@ -486,17 +491,18 @@ namespace NewAllowable
 instance hasSmulNewTangle : SMul NewAllowable NewTangle :=
   ⟨fun ρ t =>
     ⟨ρ • (t : Semitangle),
-      t.2.map fun (s : Support α NewAllowable (t : Semitangle)) =>
-        { carrier := ρ • (s : Set (SupportCondition α))
-          small := s.small.image
-          supports := by
-            intro ρ' h
-            have := s.supports (ρ⁻¹ * ρ' * ρ) ?_
-            · conv_rhs =>
-                rw [← this, ← mul_smul, ← mul_assoc, ← mul_assoc, mul_inv_self, one_mul, mul_smul]
-            · intro a ha
-              rw [mul_smul, mul_smul, inv_smul_eq_iff]
-              exact h (smul_mem_smul_set ha) }⟩⟩
+      by
+        obtain ⟨S, hS⟩ := t.2
+        refine ⟨ρ • S, ?_⟩
+        intro ρ' h
+        have := hS (ρ⁻¹ * ρ' * ρ) ?_
+        · conv_rhs =>
+            rw [← this, ← mul_smul, ← mul_assoc, ← mul_assoc, mul_inv_self, one_mul, mul_smul]
+        · intro a ha
+          rw [mul_smul, mul_smul, inv_smul_eq_iff]
+          refine h ?_
+          simp only [Support.mem_carrier_iff, smul_carrier, smul_mem_smul_set_iff] at ha ⊢
+          exact ha⟩⟩
 
 @[simp, norm_cast]
 theorem coe_smul_newTangle (ρ : NewAllowable) (t : NewTangle) :
diff --git a/ConNF/Structural/Support.lean b/ConNF/Structural/Support.lean
index d3f560f259..48b2e5487a 100644
--- a/ConNF/Structural/Support.lean
+++ b/ConNF/Structural/Support.lean
@@ -13,9 +13,9 @@ In this file, we define support conditions and supports.
 * `ConNF.Support`: The type of small supports made of support conditions.
 -/
 
-open Cardinal Equiv MulAction Quiver
+open Cardinal Equiv
 
-open scoped Cardinal
+open scoped Cardinal Pointwise
 
 universe u
 
@@ -114,41 +114,176 @@ theorem smul_supportCondition_eq_smul_iff :
 
 end NearLitterPerm
 
-variable (G : Type _) (α) {τ : Type _} [SMul G (SupportCondition α)] [SMul G τ]
+/-- A *support* is a function from an initial segment of κ to the type of support conditions. -/
+@[ext]
+structure Support (α : TypeIndex) where
+  max : κ
+  f : (i : κ) → i < max → SupportCondition α
 
-/-- A (small) support of an object is a small set of support conditions that support it. -/
-structure Support (x : τ) where
-  carrier : Set (SupportCondition α)
-  small : Small carrier
-  supports : Supports G carrier x
+def Support.carrier (S : Support α) : Set (SupportCondition α) :=
+  { c | ∃ i, ∃ (h : i < S.max), c = S.f i h }
 
-/-- An element of `τ` is *supported* if it has some support. -/
-def Supported (x : τ) : Prop :=
-  Nonempty <| Support α G x
+instance : CoeTC (Support α) (Set (SupportCondition α)) where
+  coe S := S.carrier
 
-instance Support.setLike (x : τ) : SetLike (Support α G x) (SupportCondition α)
-    where
-  coe := Support.carrier
-  coe_injective' s t h := by
-    cases s
-    cases t
-    congr
+instance : Membership (SupportCondition α) (Support α) where
+  mem c S := c ∈ S.carrier
+
+@[simp]
+theorem Support.mem_carrier_iff (c : SupportCondition α) (S : Support α) :
+    c ∈ S.carrier ↔ ∃ i, ∃ (h : i < S.max), c = S.f i h :=
+  Iff.rfl
 
 @[simp]
-theorem Support.carrier_eq_coe {x : τ} {s : Support α G x} : s.carrier = s :=
+theorem Support.mem_iff (c : SupportCondition α) (S : Support α) :
+    c ∈ S ↔ ∃ i, ∃ (h : i < S.max), c = S.f i h :=
+  Iff.rfl
+
+theorem Support.carrier_small (S : Support α) : Small S.carrier := by
+  refine lt_of_le_of_lt (b := #(Set.Iio S.max)) ?_ (card_typein_lt (· < ·) S.max Params.κ_ord.symm)
+  refine mk_le_of_surjective (f := fun x => ⟨S.f x x.prop, x, x.prop, rfl⟩) ?_
+  rintro ⟨_, i, h, rfl⟩
+  exact ⟨⟨i, h⟩, rfl⟩
+
+theorem Support.small (S : Support α) : Small (S : Set (SupportCondition α)) :=
+  S.carrier_small
+
+def supportEquiv : Support α ≃ Σ max : κ, Set.Iio max → SupportCondition α where
+  toFun S := ⟨S.max, fun x => S.f x x.prop⟩
+  invFun S := ⟨S.1, fun i h => S.2 ⟨i, h⟩⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+def funMap (α β : Type _) [LT β] (f : α → β) :
+    { S : Set β // #S ≤ #α } × (α → α → Prop) :=
+  ⟨⟨Set.range f, mk_range_le⟩, InvImage (· < ·) f⟩
+
+theorem funMap_injective {α β : Type _} [LinearOrder β] [IsWellOrder β (· < ·)] :
+    Function.Injective (funMap α β) := by
+  intro f g h
+  simp only [funMap, Prod.mk.injEq, Subtype.mk.injEq] at h
+  suffices : ∀ y : β, ∀ x : α, f x = y → g x = y
+  · ext x : 1
+    rw [this]
+    rfl
+  intro y
+  refine IsWellFounded.induction (· < ·) (C := fun y => ∀ x : α, f x = y → g x = y) y ?_
+  clear y
+  rintro y ih x rfl
+  obtain ⟨y, h₁⟩ : f x ∈ Set.range g
+  · rw [← h.1]
+    exact ⟨x, rfl⟩
+  rw [← h₁]
+  obtain (h₂ | h₂ | h₂) := lt_trichotomy (g x) (g y)
+  · obtain ⟨z, h₃⟩ : g x ∈ Set.range f
+    · rw [h.1]
+      exact ⟨x, rfl⟩
+    rw [h₁, ← h₃] at h₂
+    have h₄ := ih (f z) h₂ z rfl
+    have := congr_fun₂ h.2 z x
+    simp only [InvImage, h₂, eq_iff_iff, true_iff] at this
+    rw [h₄, h₃] at this
+    cases lt_irrefl _ this
+  · exact h₂
+  · have := congr_fun₂ h.2 y x
+    simp only [InvImage, eq_iff_iff] at this
+    rw [← this] at h₂
+    have := ih (f y) h₂ y rfl
+    have := h₂.trans_eq (h₁.symm.trans this)
+    cases lt_irrefl _ this
+
+theorem mk_fun_le {α β : Type u} :
+    #(α → β) ≤ #({ S : Set β // #S ≤ #α } × (α → α → Prop)) := by
+  classical
+  obtain ⟨r, hr⟩ := IsWellOrder.subtype_nonempty (σ := β)
+  let _ := linearOrderOfSTO r
+  exact ⟨⟨funMap α β, funMap_injective⟩⟩
+
+theorem pow_le_of_isStrongLimit' {α β : Type u} [Infinite α] [Infinite β]
+    (h₁ : IsStrongLimit #β) (h₂ : #α < (#β).ord.cof) : #β ^ #α ≤ #β := by
+  refine le_trans mk_fun_le ?_
+  simp only [mk_prod, lift_id, mk_pi, mk_fintype, Fintype.card_prop, Nat.cast_ofNat, prod_const,
+    lift_id', lift_two]
+  have h₃ : #{ S : Set β // #S ≤ #α } ≤ #β
+  · rw [← mk_subset_mk_lt_cof h₁.2]
+    refine ⟨⟨fun S => ⟨S, S.prop.trans_lt h₂⟩, ?_⟩⟩
+    intro S T h
+    simp only [Subtype.mk.injEq] at h
+    exact Subtype.coe_injective h
+  have h₄ : (2 ^ #α) ^ #α ≤ #β
+  · rw [← power_mul, mul_eq_self (Cardinal.infinite_iff.mp inferInstance)]
+    refine (h₁.2 _ ?_).le
+    exact h₂.trans_le (Ordinal.cof_ord_le #β)
+  refine le_trans (mul_le_max _ _) ?_
+  simp only [ge_iff_le, le_max_iff, max_le_iff, le_aleph0_iff_subtype_countable, h₃, h₄, and_self,
+    aleph0_le_mk]
+
+theorem pow_le_of_isStrongLimit {κ μ : Cardinal.{u}} (h₁ : IsStrongLimit μ) (h₂ : κ < μ.ord.cof) :
+    μ ^ κ ≤ μ := by
+  by_cases h : κ < ℵ₀
+  · exact pow_le h₁.isLimit.aleph0_le h
+  · revert h₁ h₂ h
+    refine inductionOn₂ κ μ ?_
+    intro α β h₁ h₂ h
+    have := Cardinal.infinite_iff.mpr (le_of_not_lt h)
+    have := Cardinal.infinite_iff.mpr h₁.isLimit.aleph0_le
+    exact pow_le_of_isStrongLimit' h₁ h₂
+
+/-- There are at most `μ` supports. -/
+theorem mk_support_le : #(Support α) ≤ #μ := by
+  rw [Cardinal.mk_congr supportEquiv]
+  simp only [mk_sigma, mk_pi, mk_supportCondition, prod_const, lift_id]
+  refine le_trans (sum_le_sum _ (fun _ => #μ) ?_) ?_
+  · intro i
+    refine pow_le_of_isStrongLimit Params.μ_isStrongLimit ?_
+    refine lt_of_lt_of_le ?_ Params.κ_le_μ_ord_cof
+    exact card_typein_lt (· < ·) i Params.κ_ord.symm
+  · simp only [sum_const, lift_id, mul_mk_eq_max, ge_iff_le, max_le_iff, le_refl, and_true]
+    exact Params.κ_lt_μ.le
+
+instance {G : Type _} [SMul G (SupportCondition α)] : SMul G (Support α) where
+  smul g S := ⟨S.max, fun i hi => g • S.f i hi⟩
+
+@[simp]
+theorem smul_max {G : Type _} [SMul G (SupportCondition α)] (g : G) (S : Support α) :
+    (g • S).max = S.max :=
+  rfl
+
+@[simp]
+theorem smul_f {G : Type _} [SMul G (SupportCondition α)]
+    (g : G) (S : Support α) (i : κ) (hi : i < S.max) :
+    (g • S).f i hi = g • S.f i hi :=
   rfl
 
-/-- There are at most `μ` supports for a given `x : τ`. -/
-theorem mk_support_le (x : τ) : #(Support α G x) ≤ #μ := by
-  trans #{ s : Set μ // Small s }
-  trans #{ S : Set (SupportCondition α) // Small S }
-  · refine ⟨⟨fun s => ⟨s.carrier, s.small⟩, fun s t h => ?_⟩⟩
-    simpa only [Subtype.mk_eq_mk, Support.carrier_eq_coe, SetLike.coe_set_eq] using h
-  · rw [← mk_subtype_of_equiv Small (Equiv.Set.congr (Cardinal.eq.mp (mk_supportCondition α)).some)]
-    refine ⟨⟨fun s => ⟨s, Small.image s.prop⟩, fun s h => ?_⟩⟩
-    simp only [Set.congr_apply, Subtype.mk.injEq]
-    exact Subtype.eq
-  · rw [← mk_subset_mk_lt_cof Params.μ_isStrongLimit.2]
-    exact mk_subtype_mono fun s hs => lt_of_lt_of_le hs Params.κ_le_μ_ord_cof
+@[simp]
+theorem smul_carrier {G : Type _} [SMul G (SupportCondition α)] (g : G) (S : Support α) :
+    (g • S).carrier = g • S.carrier := by
+  ext x : 1
+  constructor
+  · rintro ⟨i, hi, h⟩
+    exact ⟨_, ⟨i, hi, rfl⟩, h.symm⟩
+  · rintro ⟨_, ⟨i, hi, rfl⟩, h⟩
+    exact ⟨i, hi, h.symm⟩
+
+@[simp]
+theorem smul_coe {G : Type _} [SMul G (SupportCondition α)] (g : G) (S : Support α) :
+    (g • S : Support α) = g • (S : Set (SupportCondition α)) :=
+  smul_carrier g S
+
+instance {G : Type _} [Monoid G] [MulAction G (SupportCondition α)] : MulAction G (Support α) where
+  one_smul := by
+    rintro ⟨i, f⟩
+    ext
+    · rfl
+    · refine heq_of_eq (funext₂ ?_)
+      intro j hj
+      simp only [smul_f, one_smul]
+  mul_smul g h := by
+    rintro ⟨i, f⟩
+    ext
+    · rfl
+    · refine heq_of_eq (funext₂ ?_)
+      intro j hj
+      simp only [smul_f, mul_smul]
 
 end ConNF