diff --git a/ConNF/Counting/Conclusions.lean b/ConNF/Counting/Conclusions.lean
index 7017ee3199..fcbddb19c7 100644
--- a/ConNF/Counting/Conclusions.lean
+++ b/ConNF/Counting/Conclusions.lean
@@ -65,11 +65,32 @@ theorem mk_tangle_le (β : Λ) [LeLevel β] : #(Tangle β) ≤ #(TSet β) * #(Su
   simp only [Prod.mk.injEq] at h
   exact Tangle.ext t₁ t₂ h.1 h.2
 
+theorem exists_tangle [i : CountingAssumptions] {β : TypeIndex} [iβ : LeLevel β] (t : TSet β) :
+    ∃ u : Tangle β, u.set = t := by
+  revert i iβ
+  change (_ : _) → _
+  refine WithBot.recBotCoe ?_ ?_ β
+  · intro _ _ t
+    exact ⟨t, rfl⟩
+  · intro β _ _ t
+    obtain ⟨S, hS⟩ := t.has_support
+    exact ⟨⟨t, S, hS⟩, rfl⟩
+
+protected noncomputable def Tangle.typedAtom (β : Λ) [LeLevel β] (a : Atom) : Tangle β :=
+  (exists_tangle (typedAtom a)).choose
+
+protected noncomputable def Tangle.typedAtom_injective (β : Λ) [LeLevel β] :
+    Function.Injective (Tangle.typedAtom β) := by
+  intro a₁ a₂ h
+  refine (typedAtom (α := β)).injective ?_
+  rw [← (exists_tangle (typedAtom a₁)).choose_spec, ← (exists_tangle (typedAtom a₂)).choose_spec]
+  exact congr_arg Tangle.set h
+
 theorem mk_tangle (β : Λ) [LeLevel β] (hzero : #(CodingFunction 0) < #μ) : #(Tangle β) = #μ := by
   refine le_antisymm ?_ ?_
   · refine le_trans (mk_tangle_le β) ?_
     exact mul_le_of_le (mk_tSet_le β hzero) mk_support.le Params.μ_isStrongLimit.isLimit.aleph0_le
-  · have := mk_le_of_injective (typedAtom (α := β)).injective
+  · have := mk_le_of_injective (Tangle.typedAtom_injective β)
     simp only [mk_atom] at this
     exact this
 
diff --git a/ConNF/FOA/Basic/Constrains.lean b/ConNF/FOA/Basic/Constrains.lean
index 5409892505..e195a7b196 100644
--- a/ConNF/FOA/Basic/Constrains.lean
+++ b/ConNF/FOA/Basic/Constrains.lean
@@ -77,16 +77,12 @@ theorem Constrains.hasPosition_lt {c d : Address β} (h : c ≺ d) :
     have := pos_lt_pos_fuzz_nearLitter hδε t (ConNF.fuzz hδε t).toNearLitter rfl
     obtain ⟨B, a | N⟩ := c
     · simp only [Address.pos_atom, Address.pos_nearLitter]
-      by_cases h : t = typedAtom a
-      · subst h
-        rw [pos_typedAtom] at this
-        exact this
+      by_cases h : t.set = typedAtom a
+      · exact (pos_typedAtom a t h).trans_lt this
       · exact (pos_lt_pos_atom _ hc' h).trans this
     · simp only [Address.pos_nearLitter]
-      by_cases h : t = typedNearLitter N
-      · subst h
-        rw [pos_typedNearLitter] at this
-        exact this
+      by_cases h : t.set = typedNearLitter N
+      · exact (pos_typedNearLitter N t h).trans_lt this
       · exact (pos_lt_pos_nearLitter _ hc' h).trans this
   case fuzzBot γ _ ε _ hε A a =>
     simp only [Address.pos_atom, Address.pos_nearLitter]
diff --git a/ConNF/FOA/Basic/Hypotheses.lean b/ConNF/FOA/Basic/Hypotheses.lean
index 1a6cd9160a..e54e43c751 100644
--- a/ConNF/FOA/Basic/Hypotheses.lean
+++ b/ConNF/FOA/Basic/Hypotheses.lean
@@ -139,11 +139,11 @@ class FOAAssumptions extends FOAData where
   /-- Inflexible litters whose atoms occur in designated supports have position less than the
   original tangle. -/
   pos_lt_pos_atom {β : Λ} [LtLevel β] (t : Tangle β) {A : ExtendedIndex β} {a : Atom} :
-    ⟨A, Sum.inl a⟩ ∈ t.support → t ≠ typedAtom a → pos a < pos t
+    ⟨A, Sum.inl a⟩ ∈ t.support → t.set ≠ typedAtom a → pos a < pos t
   /-- Inflexible litters touching near-litters in designated supports have position less than the
   original tangle. -/
   pos_lt_pos_nearLitter {β : Λ} [LtLevel β] (t : Tangle β) {A : ExtendedIndex β} {N : NearLitter} :
-    ⟨A, Sum.inr N⟩ ∈ t.support → t ≠ typedNearLitter N → pos N < pos t
+    ⟨A, Sum.inr N⟩ ∈ t.support → t.set ≠ typedNearLitter N → pos N < pos t
   /-- The `fuzz` map commutes with allowable permutations. -/
   smul_fuzz {β : TypeIndex} [LeLevel β] {γ : TypeIndex} [LtLevel γ] {δ : Λ} [LtLevel δ]
     (hγ : γ < β) (hδ : (δ : TypeIndex) < β) (hγδ : γ ≠ δ) (ρ : Allowable β) (t : Tangle γ) :
diff --git a/ConNF/Fuzz/Hypotheses.lean b/ConNF/Fuzz/Hypotheses.lean
index 82bf73831e..02af4d972e 100644
--- a/ConNF/Fuzz/Hypotheses.lean
+++ b/ConNF/Fuzz/Hypotheses.lean
@@ -198,10 +198,10 @@ with the conditions given in `BasePositions`, but this requirement is expressed
 class TypedObjects where
   /-- Encode an atom as an `α`-tangle. The resulting model element has a `⊥`-extension which
   contains only this atom. -/
-  typedAtom : Atom ↪ Tangle α
+  typedAtom : Atom ↪ TSet α
   /-- Encode a near-litter as an `α`-tangle. The resulting model element has a `⊥`-extension which
   contains only this near-litter. -/
-  typedNearLitter : NearLitter ↪ Tangle α
+  typedNearLitter : NearLitter ↪ TSet α
   smul_typedNearLitter :
     ∀ (ρ : Allowable α) (N : NearLitter),
     ρ • typedNearLitter N =
@@ -239,13 +239,13 @@ theorem lt_pos_symmDiff [BasePositions] (a : Atom) (N : NearLitter) (h : a ∈ l
   BasePositions.lt_pos_symmDiff a N h
 
 class PositionedObjects [BasePositions] [PositionedTangles α] [TypedObjects α] where
-  pos_typedAtom (a : Atom) : pos (typedAtom a : Tangle α) = pos a
-  pos_typedNearLitter (N : NearLitter) : pos (typedNearLitter N : Tangle α) = pos N
+  pos_typedAtom (a : Atom) (t : Tangle α) :
+    t.set = typedAtom a → pos a ≤ pos t
+  pos_typedNearLitter (N : NearLitter) (t : Tangle α) :
+    t.set = typedNearLitter N → pos N ≤ pos t
 
 export PositionedObjects (pos_typedAtom pos_typedNearLitter)
 
-attribute [simp] pos_typedAtom pos_typedNearLitter
-
 namespace Allowable
 
 variable {α}
@@ -254,7 +254,7 @@ variable [TypedObjects α]
 /-- The action of allowable permutations on tangles commutes with the `typedNearLitter` function
 mapping near-litters to typed near-litters. This can be seen by representing tangles as codes. -/
 theorem smul_typedNearLitter (ρ : Allowable α) (N : NearLitter) :
-    (ρ • typedNearLitter N : Tangle α) =
+    (ρ • typedNearLitter N : TSet α) =
     typedNearLitter ((Allowable.toStructPerm ρ) (Quiver.Hom.toPath <| bot_lt_coe α) • N) :=
   TypedObjects.smul_typedNearLitter _ _
 
diff --git a/ConNF/Model/Construction.lean b/ConNF/Model/Construction.lean
index 7634e34e7e..0c91c9486e 100644
--- a/ConNF/Model/Construction.lean
+++ b/ConNF/Model/Construction.lean
@@ -1,6 +1,5 @@
 import ConNF.NewTangle
 import ConNF.Counting
-import ConNF.Model.PretangleEmbedding
 
 open Cardinal Function MulAction Set Sum Quiver WithBot
 
diff --git a/ConNF/Model/PretangleEmbedding.lean b/ConNF/Model/PretangleEmbedding.lean
deleted file mode 100644
index 9376e3f0a7..0000000000
--- a/ConNF/Model/PretangleEmbedding.lean
+++ /dev/null
@@ -1,97 +0,0 @@
-import ConNF.NewTangle
-import ConNF.Counting.Hypotheses
-
-open Cardinal Function MulAction Set Sum Quiver WithBot
-
-open scoped Cardinal Pointwise
-
-universe u
-
-namespace ConNF
-
-variable [Params.{u}] [BasePositions] [Level]
-  [TangleDataLt] [PositionedTanglesLt] [TypedObjectsLt] [PositionedObjectsLt]
-
-def Semitangle.toPretangle (t : Semitangle)
-  (lower : ∀ (β : TypeIndex) [LtLevel β], Tangle β → Pretangle β) : Pretangle α :=
-  Pretangle.ofCoe.symm
-    (fun β hβ => match β with
-      | ⊥ => {a | ∃ s : Set Atom, ∃ h, t.pref = Preference.base s h ∧ a ∈ s}
-      | (β : Λ) => letI : LtLevel β := ⟨hβ⟩; {p | ∃ s ∈ t.members β, lower β s = p})
-
-def NewTangle.toPretangle (t : NewTangle)
-  (lower : ∀ (β : TypeIndex) [LtLevel β], Tangle β → Pretangle β) : Pretangle α :=
-  t.t.toPretangle lower
-
-theorem Semitangle.toPretangle_smul (ρ : NewAllowable) (t : Semitangle)
-    (lower : ∀ (β : TypeIndex) [LtLevel β], Tangle β → Pretangle β)
-    (h : ∀ (β : TypeIndex) [LtLevel β] (ρ' : Allowable β) (t' : Tangle β),
-      ρ' • lower β t' = lower β (ρ' • t')) :
-    ρ • t.toPretangle lower = (ρ • t).toPretangle lower := by
-  rw [← Pretangle.ofCoe_inj, toPretangle, toPretangle]
-  rw [Equiv.apply_symm_apply]
-  ext β hβ : 2
-  revert hβ
-  refine WithBot.recBotCoe ?_ ?_ β
-  · intro hβ
-    rw [← NewAllowable.coe_smul]
-    erw [StructPerm.ofCoe_smul]
-    rw [Equiv.apply_symm_apply]
-    dsimp only
-    ext a : 1
-    rw [mem_smul_set_iff_inv_smul_mem]
-    constructor
-    · rintro ⟨s, h, hpref, ha⟩
-      refine ⟨Tree.comp (Hom.toPath hβ) (SemiallowablePerm.toStructPerm ρ.val) • s, ?_, ?_, ?_⟩
-      · intro γ _
-        have := NewAllowable.smul_cloud (β := ⊥) (γ := γ) ρ s bot_ne_coe
-        rw [h] at this
-        exact this.symm
-      · obtain ⟨exts, pref | pref⟩ := t
-        · cases hpref
-          rfl
-        · cases hpref
-      · rw [mem_smul_set_iff_inv_smul_mem]
-        exact ha
-    · rintro ⟨s, h, hpref, ha⟩
-      refine ⟨(Tree.comp (Hom.toPath hβ) (SemiallowablePerm.toStructPerm ρ.val))⁻¹ • s, ?_, ?_, ?_⟩
-      · intro γ _
-        have := NewAllowable.smul_cloud (β := ⊥) (γ := γ)
-          ρ ((Tree.comp (Hom.toPath hβ) (SemiallowablePerm.toStructPerm ρ.val))⁻¹ • s) bot_ne_coe
-        rw [SemiallowablePerm.comp_toPath_toStructPerm] at this
-        erw [smul_inv_smul] at this
-        rw [h, NewAllowable.members_smul'] at this
-        erw [smul_left_cancel_iff] at this
-        exact this
-      · obtain ⟨exts, pref | pref⟩ := t
-        · cases hpref
-          simp only [Tree.comp_bot, Tree.toBot_inv_smul, Preference.base.injEq]
-          erw [smul_inv_smul]
-        · cases hpref
-      · simp only [Tree.comp_bot, Tree.toBot_inv_smul, smul_mem_smul_set_iff]
-        exact ha
-  · intro β hβ
-    have : LtLevel β := ⟨hβ⟩
-    rw [← NewAllowable.coe_smul]
-    erw [StructPerm.ofCoe_smul]
-    rw [Equiv.apply_symm_apply]
-    dsimp only
-    ext s : 1
-    constructor
-    · rintro ⟨_, ⟨s, hs, rfl⟩, rfl⟩
-      refine ⟨ρ.val β • s, smul_mem_smul_set hs, ?_⟩
-      rw [← h, SemiallowablePerm.comp_toPath_toStructPerm]
-      rfl
-    · rintro ⟨_, ⟨s, hs, rfl⟩, rfl⟩
-      refine ⟨_, ⟨s, hs, rfl⟩, ?_⟩
-      rw [← h, SemiallowablePerm.comp_toPath_toStructPerm]
-      rfl
-
-theorem NewTangle.toPretangle_smul (ρ : NewAllowable) (t : NewTangle)
-    (lower : ∀ (β : TypeIndex) [LtLevel β], Tangle β → Pretangle β)
-    (h : ∀ (β : TypeIndex) [LtLevel β] (ρ' : Allowable β) (t' : Tangle β),
-      ρ' • lower β t' = lower β (ρ' • t')) :
-    ρ • t.toPretangle lower = (ρ • t).toPretangle lower :=
-  t.t.toPretangle_smul ρ lower h
-
-end ConNF
diff --git a/ConNF/NewTangle/Cloud.lean b/ConNF/NewTangle/Cloud.lean
index bf562f90ae..b686bc5975 100644
--- a/ConNF/NewTangle/Cloud.lean
+++ b/ConNF/NewTangle/Cloud.lean
@@ -43,44 +43,36 @@ open Code
 
 section Cloud
 
-variable {γ : TypeIndex} [LtLevel γ] [TangleData γ] [PositionedTangles γ]
-  {β : Λ} [LtLevel β] [TangleData β] [PositionedTangles β] [TypedObjects β] [PositionedObjects β]
+variable [TangleDataLt] [PositionedTanglesLt] [TypedObjectsLt] [PositionedObjectsLt]
+  {γ : TypeIndex} [LtLevel γ] {β : Λ} [LtLevel β]
   (hγβ : γ ≠ β)
 
+-- TODO: Remove `localCardinal`
+
 /-- The cloud map. We map each tangle to all typed near-litters near the `fuzz`ed tangle, and take
 the union over all tangles in the input. -/
-def cloud (s : Set (Tangle γ)) : Set (Tangle β) :=
-  typedNearLitter '' ⋃ t ∈ s, localCardinal (fuzz hγβ t)
+def cloud (s : Set (TSet γ)) : Set (TSet β) :=
+  {u | ∃ t : Tangle γ, t.set_lt ∈ s ∧
+    ∃ N : NearLitter,  N.1 = fuzz hγβ t ∧ u = typedNearLitter N}
 
 variable {hγβ}
 
 @[simp]
-theorem mem_cloud {t : Tangle β} {s : Set (Tangle γ)} :
-    t ∈ cloud hγβ s ↔
-      ∃ t' ∈ s, ∃ (N : NearLitter), N.1 = fuzz hγβ t' ∧ t = typedNearLitter N := by
-  simp only [cloud, mem_image, mem_iUnion, mem_localCardinal, exists_prop]
-  constructor
-  · rintro ⟨N, ⟨t, ht₁, ht₂⟩, rfl⟩
-    exact ⟨t, ht₁, N, ht₂, rfl⟩
-  · rintro ⟨t, ht₁, N, ht₂, rfl⟩
-    exact ⟨N, ⟨t, ht₁, ht₂⟩, rfl⟩
-
-@[simp]
-theorem cloud_empty : cloud hγβ (∅ : Set (Tangle γ)) = ∅ := by
-  simp only [cloud, mem_empty_iff_false, iUnion_of_empty, iUnion_empty, image_empty]
+theorem cloud_empty : cloud hγβ (∅ : Set (TSet γ)) = ∅ := by
+  simp only [cloud, mem_empty_iff_false, false_and, exists_false, setOf_false]
 
 @[simp]
-theorem cloud_singleton (t : Tangle γ) :
-    cloud hγβ {t} = typedNearLitter '' localCardinal (fuzz hγβ t) := by
-  simp only [cloud, mem_singleton_iff, iUnion_iUnion_eq_left]
+theorem cloud_singleton (t : TSet γ) :
+    cloud hγβ {t} = {u | ∃ t' : Tangle γ, t'.set_lt = t ∧
+      ∃ N : NearLitter,  N.1 = fuzz hγβ t' ∧ u = typedNearLitter N} := by
+  simp only [cloud, mem_singleton_iff, exists_eq_left]
 
-variable {s : Set (Tangle γ)} {t : Tangle γ}
+variable {s : Set (TSet γ)} {t : TSet γ}
 
 theorem _root_.Set.Nonempty.cloud (h : s.Nonempty) : (cloud hγβ s).Nonempty := by
-  refine (nonempty_iUnion.2 ?_).image _
-  refine ⟨h.choose, ⟨(fuzz hγβ h.choose).toNearLitter, ?_⟩⟩
-  simp only [mem_iUnion, mem_localCardinal, Litter.toNearLitter_fst, exists_prop, and_true]
-  exact h.choose_spec
+  obtain ⟨u, hu⟩ := h
+  obtain ⟨u, rfl⟩ := exists_tangle_lt u
+  exact ⟨_, u, hu, (fuzz hγβ u).toNearLitter, rfl, rfl⟩
 
 @[simp]
 theorem cloud_eq_empty (hγβ : γ ≠ β) : cloud hγβ s = ∅ ↔ s = ∅ := by
@@ -92,29 +84,49 @@ theorem cloud_eq_empty (hγβ : γ ≠ β) : cloud hγβ s = ∅ ↔ s = ∅ :=
 theorem cloud_nonempty (hγβ : γ ≠ β) : (cloud hγβ s).Nonempty ↔ s.Nonempty := by
   simp_rw [nonempty_iff_ne_empty, Ne.def, cloud_eq_empty]
 
-theorem subset_cloud (ht : t ∈ s) :
-    typedNearLitter '' localCardinal (fuzz hγβ t) ⊆ cloud hγβ s :=
-  image_subset _ <| subset_iUnion₂ (s := fun t' _ => localCardinal (fuzz hγβ t')) t ht
+theorem subset_cloud (t : Tangle γ) (ht : t.set_lt ∈ s) :
+    typedNearLitter '' localCardinal (fuzz hγβ t) ⊆ cloud hγβ s := by
+  rintro _ ⟨N, hN, rfl⟩
+  exact ⟨t, ht, N, hN, rfl⟩
 
 theorem μ_le_mk_cloud : s.Nonempty → #μ ≤ #(cloud hγβ s) := by
   rintro ⟨t, ht⟩
-  refine' (Cardinal.mk_le_mk_of_subset <| subset_cloud ht).trans_eq' _
+  obtain ⟨t, rfl⟩ := exists_tangle_lt t
+  refine' (Cardinal.mk_le_mk_of_subset <| subset_cloud t ht).trans_eq' _
   rw [Cardinal.mk_image_eq, mk_localCardinal]
   exact typedNearLitter.inj'
 
-theorem cloud_injective : Injective (cloud hγβ) :=
-  typedNearLitter.injective.image_injective.comp <|
-    Pairwise.biUnion_injective (fun _ _ h => localCardinal_disjoint <| (fuzz_injective _).ne h)
-      fun _ => localCardinal_nonempty _
-
-variable {δ : TypeIndex} [LtLevel δ] [TangleData δ] [PositionedTangles δ]
-
-theorem cloud_disjoint_range {hδβ} (c : Set (Tangle γ)) (d : Set (Tangle δ)) (hc : c.Nonempty)
+theorem subset_of_cloud_subset (s₁ s₂ : Set (TSet γ)) (h : cloud hγβ s₁ ⊆ cloud hγβ s₂) :
+    s₁ ⊆ s₂ := by
+  contrapose h
+  rw [not_subset] at h ⊢
+  obtain ⟨t, h₁, h₂⟩ := h
+  obtain ⟨t, rfl⟩ := exists_tangle_lt t
+  refine ⟨typedNearLitter (fuzz hγβ t).toNearLitter, ?_, ?_⟩
+  · refine ⟨t, h₁, _, by exact rfl, rfl⟩
+  · contrapose! h₂
+    obtain ⟨u, hu, N, hN₁, hN₂⟩ := h₂
+    cases typedNearLitter.injective hN₂
+    cases fuzz_injective hγβ hN₁
+    exact hu
+
+theorem cloud_injective : Injective (cloud hγβ) := by
+  intro s₁ s₂ h
+  refine subset_antisymm ?_ ?_
+  exact subset_of_cloud_subset s₁ s₂ (subset_of_eq h)
+  exact subset_of_cloud_subset s₂ s₁ (subset_of_eq h.symm)
+
+variable {δ : TypeIndex} [LtLevel δ]
+
+theorem cloud_disjoint_range {hδβ} (c : Set (TSet γ)) (d : Set (TSet δ)) (hc : c.Nonempty)
     (h : cloud hγβ c = cloud hδβ d) : γ = δ := by
   obtain ⟨b, hb⟩ := hc
-  have := (subset_iUnion₂ b hb).trans (typedNearLitter.injective.image_injective h).subset
-  obtain ⟨i, -, hi⟩ := mem_iUnion₂.1 (this (fuzz _ b).toNearLitter_mem_localCardinal)
-  exact fuzz_congr_β hi
+  obtain ⟨b, rfl⟩ := exists_tangle_lt b
+  have := (Set.ext_iff.mp h (typedNearLitter (fuzz hγβ b).toNearLitter)).mp
+    ⟨b, hb, _, by exact rfl, rfl⟩
+  obtain ⟨b', _, N, hN₁, hN₂⟩ := this
+  cases typedNearLitter.injective hN₂
+  exact fuzz_congr_β hN₁
 
 /-!
 We don't need to prove that the ranges of the `cloud` maps are disjoint for different `β`, since
@@ -138,12 +150,23 @@ theorem minTangle_le (s : Set (Tangle γ)) (hs : s.Nonempty) {t : Tangle γ} (ht
     pos (minTangle s hs) ≤ pos t :=
   not_lt.1 <| wellFounded_pos.not_lt_min s hs ht
 
-theorem minTangle_lt_minTangle_cloud (s : Set (Tangle γ)) (hs : s.Nonempty) :
-    pos (minTangle s hs) < pos (minTangle (cloud hγβ s) hs.cloud) := by
-  obtain ⟨t, ht, N, hN, h⟩ := mem_cloud.1 (minTangle_mem (cloud hγβ s) hs.cloud)
-  refine (minTangle_le s hs ht).trans_lt ?_
-  rw [h, pos_typedNearLitter]
-  exact pos_lt_pos_fuzz_nearLitter hγβ t _ hN
+theorem set_invImage_nonempty (s : Set (TSet γ)) (hs : s.Nonempty) :
+    (Tangle.set_lt ⁻¹' s).Nonempty := by
+  obtain ⟨t, ht⟩ := hs
+  obtain ⟨t, rfl⟩ := exists_tangle_lt t
+  exact ⟨t, ht⟩
+
+noncomputable def minTSet (s : Set (TSet γ)) (hs : s.Nonempty) : Tangle γ :=
+  minTangle (Tangle.set_lt ⁻¹' s) (set_invImage_nonempty s hs)
+
+theorem minTSet_lt_minTSet_cloud (s : Set (TSet γ)) (hs : s.Nonempty) :
+    pos (minTSet s hs) < pos (minTSet (cloud hγβ s) hs.cloud) := by
+  obtain ⟨t, ht, N, hN, h⟩ := minTangle_mem (Tangle.set_lt ⁻¹' cloud hγβ s)
+    (set_invImage_nonempty _ hs.cloud)
+  have := pos_typedNearLitter N
+    (minTangle (Tangle.set_lt ⁻¹' cloud hγβ s) (set_invImage_nonempty _ hs.cloud)) h
+  refine lt_of_le_of_lt (minTangle_le _ _ ht) ?_
+  exact (pos_lt_pos_fuzz_nearLitter hγβ t _ hN).trans_le this
 
 end Cloud
 
@@ -154,7 +177,7 @@ variable [TangleDataLt] [PositionedTanglesLt]
 /-- Tool that lets us use well-founded recursion on codes via `μ`.
 This maps a nonempty code to the least pos of a tangle in the extension of the code. -/
 noncomputable def codeMinMap (c : NonemptyCode) : μ :=
-  pos <| minTangle _ c.prop
+  pos <| minTSet _ c.prop
 
 /-- The pullback `<` relation on codes is well-founded. -/
 theorem invImage_codeMinMap_wf : WellFounded (InvImage (· < ·) (codeMinMap : NonemptyCode → μ)) :=
@@ -166,14 +189,14 @@ variable [TypedObjectsLt] {β : TypeIndex} [LtLevel β]
 
 /-- The `cloud` map, phrased as a function on sets of `γ`-tangles, but if `γ = β`, this is the
 identity function. -/
-def extension (s : Set (Tangle β)) (γ : Λ) [LtLevel γ] : Set (Tangle γ) :=
+def extension (s : Set (TSet β)) (γ : Λ) [LtLevel γ] : Set (TSet γ) :=
   if hβγ : β = γ then cast (by subst hβγ; rfl) s else cloud hβγ s
 
 @[simp]
-theorem extension_self {γ : Λ} [LtLevel γ] (s : Set (Tangle γ)) : extension s γ = s :=
+theorem extension_self {γ : Λ} [LtLevel γ] (s : Set (TSet γ)) : extension s γ = s :=
   dif_pos rfl
 
-variable (s : Set (Tangle β)) (γ : Λ) [LtLevel γ]
+variable (s : Set (TSet β)) (γ : Λ) [LtLevel γ]
 
 @[simp]
 theorem extension_eq (hβγ : β = γ) : extension s γ = cast (by subst hβγ; rfl) s :=
@@ -258,10 +281,9 @@ theorem codeMinMap_lt_codeMinMap_cloudCode (c : NonemptyCode) (hcβ : c.1.1 ≠
     codeMinMap c < codeMinMap ⟨cloudCode β c, cloudCode_nonempty.mpr c.2⟩ := by
   unfold codeMinMap
   have := cloudCode_ne β c hcβ
-  convert minTangle_lt_minTangle_cloud c.1.members c.2 using 1
+  convert minTSet_lt_minTSet_cloud c.1.members c.2 using 1
   congr
   exact snd_cloudCode β c hcβ
-  infer_instance
 
 /-- This relation on `α`-codes allows us to state that there are only finitely many iterated images
 under the inverse `cloud` map. Note that we require the map to actually change the data, by
diff --git a/ConNF/NewTangle/Code.lean b/ConNF/NewTangle/Code.lean
index b239e2f9f3..421421288e 100644
--- a/ConNF/NewTangle/Code.lean
+++ b/ConNF/NewTangle/Code.lean
@@ -17,14 +17,14 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [TangleDataLt] {β : Λ} [LtLevel β] {s t : Set (Tangle β)}
+variable [Params.{u}] [Level] [TangleDataLt] {β : Λ} [LtLevel β] {s t : Set (TSet β)}
 
 /-- An `α` code is a type index `β < α` together with a set of tangles of type `β`. -/
 @[ext]
 structure Code : Type u where
   (β : TypeIndex)
   [inst : LtLevel β]
-  (members : Set (Tangle β))
+  (members : Set (TSet β))
 
 instance (c : Code) : LtLevel c.β := c.inst
 
diff --git a/ConNF/NewTangle/CodeEquiv.lean b/ConNF/NewTangle/CodeEquiv.lean
index 597549909d..29c1facff6 100644
--- a/ConNF/NewTangle/CodeEquiv.lean
+++ b/ConNF/NewTangle/CodeEquiv.lean
@@ -329,45 +329,8 @@ theorem bot_bot_iff {s t} : (mk ⊥ s : Code) ≡ mk ⊥ t ↔ s = t := by
   · rintro rfl
     rfl
 
-theorem singleton (hβγ : β ≠ γ) (g : Tangle β) :
-    mk β {g} ≡ mk γ (typedNearLitter '' localCardinal (fuzz hβγ g)) := by
-  convert Equiv.cloud_right (mk β {g}) (isEven_singleton _) _ hβγ
-  aesop
-
-theorem singleton_iff {g} :
-    c ≡ mk β {g} ↔
-    c = mk β {g} ∨ ∃ γ : Λ, ∃ _ : LtLevel γ,
-      (c.1 : TypeIndex) = (γ : Λ) ∧ β ≠ γ ∧ c = cloudCode γ (mk β {g}) := by
-  classical
-  refine ⟨fun h => ?_, ?_⟩
-  · rw [equiv_iff] at h
-    simp only [isEven_singleton, ne_eq, exists_and_left, true_and] at h
-    obtain rfl | ⟨γ, hβγ, _, _, rfl⟩ | ⟨_, γ, γne, _, h⟩ | ⟨d, -, γ, _, _, δ, δne, _, _, h⟩ :=
-      h
-    · exact Or.inl rfl
-    · simp only [Subtype.coe_mk, SetCoe.exists, exists_and_left]
-      exact Or.inr ⟨_, rfl, hβγ, inferInstance, rfl⟩
-    · cases congr_arg Code.β h
-      cases cloudCode_ne_singleton γne h.symm
-    · cases congr_arg Code.β h
-      cases cloudCode_ne_singleton δne h.symm
-  · rintro (rfl | ⟨γ, _, hc, hβγ, rfl⟩)
-    · rfl
-    · convert (singleton hβγ g).symm
-      simp only [cloudCode, ne_eq, extension_ne _ _ hβγ, cloud_singleton]
-
 end Equiv
 
-theorem extension_eq_of_singleton_equiv_singleton {γ : TypeIndex} [LtLevel γ]
-    {a : Tangle β} {b : Tangle γ}
-    (h : (⟨β, {a}⟩ : Code) ≡ ⟨γ, {b}⟩) : β = γ := by
-  obtain h | ⟨ε, _, hc, hβε, hA⟩ := Equiv.singleton_iff.1 h
-  · exact ((Code.ext_iff _ _).1 h).1
-  · exfalso
-    refine cloudCode_ne_singleton ?_ hA.symm
-    cases congr_arg Code.β hA
-    exact hβε
-
 theorem IsEven.unique : ∀ {c d : Code}, c.IsEven → d.IsEven → c ≡ d → c = d
   | c, _, _, _, Equiv.refl _ => rfl
   | _, _, _, _, Equiv.cloud_left d hd β hdβ => by cases (hd.cloudCode hdβ).not_isEven ‹_›
diff --git a/ConNF/NewTangle/Hypotheses.lean b/ConNF/NewTangle/Hypotheses.lean
index 4e2eb3248a..01fa15a646 100644
--- a/ConNF/NewTangle/Hypotheses.lean
+++ b/ConNF/NewTangle/Hypotheses.lean
@@ -52,4 +52,39 @@ abbrev TypedObjectsLt [TangleDataLt] :=
 abbrev PositionedObjectsLt [BasePositions] [TangleDataLt] [PositionedTanglesLt] [TypedObjectsLt] :=
   ∀ β : Λ, [LtLevel β] → PositionedObjects β
 
+/-! We have to give the following things different names in the two places we define them:
+here, and in the FOA hypothesis file. -/
+
+def Tangle.set_lt [TangleDataLt] : {β : TypeIndex} → [LtLevel β] → Tangle β → TSet β
+  | (β : Λ), _, t => TangleCoe.set t
+  | ⊥, _i, a => a
+
+theorem exists_tangle_lt [i : TangleDataLt] {β : TypeIndex} [iβ : LtLevel β] (t : TSet β) :
+    ∃ u : Tangle β, u.set_lt = t := by
+  revert i iβ
+  change (_ : _) → _
+  refine WithBot.recBotCoe ?_ ?_ β
+  · intro _ _ t
+    exact ⟨t, rfl⟩
+  · intro β _ _ t
+    obtain ⟨S, hS⟩ := t.has_support
+    exact ⟨⟨t, S, hS⟩, rfl⟩
+
+theorem Tangle.ext_lt [i : TangleDataLt] {β : TypeIndex} [iβ : LtLevel β] (t₁ t₂ : Tangle β)
+    (hs : t₁.set_lt = t₂.set_lt) (hS : t₁.support = t₂.support) : t₁ = t₂ := by
+  revert i iβ t₁ t₂
+  change (_ : _) → _
+  refine WithBot.recBotCoe ?_ ?_ β
+  · intro _ _ t₁ t₂ hs _
+    exact hs
+  · intro β _ _ t₁ t₂ hs hS
+    exact TangleCoe.ext _ _ hs hS
+
+theorem Tangle.smul_set_lt [i : TangleDataLt] {β : TypeIndex} [iβ : LtLevel β]
+    (t : Tangle β) (ρ : Allowable β) :
+    (ρ • t).set_lt = ρ • t.set_lt := by
+  revert i iβ
+  change (_ : _) → _
+  refine WithBot.recBotCoe ?_ ?_ β <;> intros <;> rfl
+
 end ConNF
diff --git a/ConNF/NewTangle/NewAllowable.lean b/ConNF/NewTangle/NewAllowable.lean
index 46cab25abf..f8d3309a7f 100644
--- a/ConNF/NewTangle/NewAllowable.lean
+++ b/ConNF/NewTangle/NewAllowable.lean
@@ -209,7 +209,7 @@ theorem members_smul : (ρ • c).members = ρ c.1 • c.members :=
   rfl
 
 @[simp]
-theorem smul_mk (f : SemiallowablePerm) (γ : TypeIndex) [LtLevel γ] (s : Set (Tangle γ)) :
+theorem smul_mk (f : SemiallowablePerm) (γ : TypeIndex) [LtLevel γ] (s : Set (TSet γ)) :
     f • (mk γ s : Code) = mk γ (f γ • s) :=
   rfl
 
@@ -372,7 +372,7 @@ end
 
 @[simp]
 theorem smul_typedNearLitter (ρ : NewAllowable) (N : NearLitter) :
-    ρ.val γ • (typedNearLitter N : Tangle (γ : Λ)) =
+    ρ.val γ • (typedNearLitter N : TSet (γ : Λ)) =
     typedNearLitter ((Allowable.toStructPerm ((ρ : SemiallowablePerm) γ)
       (Quiver.Hom.toPath (bot_lt_coe _))) • N) :=
   Allowable.smul_typedNearLitter _ _
@@ -386,7 +386,7 @@ theorem members_smul (ρ : NewAllowable) (c : Code) : (ρ • c).members = ρ.va
   rfl
 
 @[simp]
-theorem smul_mk (ρ : NewAllowable) (γ : TypeIndex) [LtLevel γ] (s : Set (Tangle γ)) :
+theorem smul_mk (ρ : NewAllowable) (γ : TypeIndex) [LtLevel γ] (s : Set (TSet γ)) :
     ρ • (mk γ s : Code) = mk γ (ρ.val γ • s) :=
   rfl
 
@@ -396,14 +396,7 @@ namespace NewAllowable
 
 variable {β γ}
 
-/-- Allowable permutations commute with the `cloud` map. -/
-theorem smul_cloud (ρ : NewAllowable) (s : Set (Tangle β)) (hβγ : β ≠ γ) :
-    ρ.val γ • cloud hβγ s = cloud hβγ (ρ.val β • s) := by
-  ext t
-  simp only [cloud, mem_image, mem_iUnion, mem_localCardinal, exists_prop, ← image_smul]
-  simp_rw [exists_exists_and_eq_and]
-  constructor
-  · rintro ⟨N, ⟨t, ht₁, ht₂⟩, rfl⟩
+/-   · rintro ⟨N, ⟨t, ht₁, ht₂⟩, rfl⟩
     refine ⟨Allowable.toStructPerm ((ρ : SemiallowablePerm) γ)
         (Quiver.Hom.toPath <| bot_lt_coe _) • N, ⟨t, ht₁, ?_⟩, ?_⟩
     · rw [← ρ.prop hβγ, NearLitterPerm.smul_nearLitter_fst, ht₂]
@@ -414,6 +407,36 @@ theorem smul_cloud (ρ : NewAllowable) (s : Set (Tangle β)) (hβγ : β ≠ γ)
     · rw [NearLitterPerm.smul_nearLitter_fst, ht₂, ← ρ.prop hβγ, map_inv,
         Tree.inv_apply, inv_smul_smul]
     · rw [smul_typedNearLitter, map_inv, Tree.inv_apply, smul_inv_smul]
+ -/
+
+/-- Allowable permutations commute with the `cloud` map. -/
+theorem smul_cloud (ρ : NewAllowable) (s : Set (TSet β)) (hβγ : β ≠ γ) :
+    ρ.val γ • cloud hβγ s = cloud hβγ (ρ.val β • s) := by
+  ext t
+  constructor
+  · rintro ⟨_, ⟨t, ht, N, hN, rfl⟩, rfl⟩
+    refine ⟨ρ.val β • t, ?_,
+        Allowable.toStructPerm ((ρ : SemiallowablePerm) γ)
+          (Quiver.Hom.toPath (bot_lt_coe _)) • N, ?_, ?_⟩
+    · rw [Tangle.smul_set_lt, smul_mem_smul_set_iff]
+      exact ht
+    · rw [← ρ.prop hβγ, NearLitterPerm.smul_nearLitter_fst, hN]
+    · dsimp only
+      rw [smul_typedNearLitter]
+  · rintro ⟨t, ht, N, hN, rfl⟩
+    refine ⟨typedNearLitter ((Allowable.toStructPerm ((ρ : SemiallowablePerm) γ)
+          (Quiver.Hom.toPath (bot_lt_coe _)))⁻¹ • N),
+        ⟨(ρ.val β)⁻¹ • t, ?_, ?_⟩, ?_⟩
+    · rw [Tangle.smul_set_lt, ← mem_smul_set_iff_inv_smul_mem]
+      exact ht
+    · refine ⟨(Allowable.toStructPerm ((ρ : SemiallowablePerm) γ)
+        (Quiver.Hom.toPath (bot_lt_coe _)))⁻¹ • N, ?_, rfl⟩
+      refine Eq.trans ?_ (ρ⁻¹.prop hβγ t)
+      simp only [NearLitterPerm.smul_nearLitter_fst, coe_inv, SemiallowablePerm.inv_apply,
+        map_inv, Tree.inv_apply, smul_left_cancel_iff]
+      exact hN
+    · dsimp only
+      rw [smul_typedNearLitter, smul_inv_smul]
 
 /-- Allowable permutations commute with the `cloudCode` map. -/
 theorem smul_cloudCode (ρ : NewAllowable) (hc : c.1 ≠ γ) :
diff --git a/ConNF/NewTangle/NewTangle.lean b/ConNF/NewTangle/NewTangle.lean
index 27e5c77a96..d8cbbfe10b 100644
--- a/ConNF/NewTangle/NewTangle.lean
+++ b/ConNF/NewTangle/NewTangle.lean
@@ -34,7 +34,7 @@ variable [Params.{u}] [Level] [BasePositions] [TangleDataLt]
 open Code
 
 abbrev Extensions :=
-  ∀ β : Λ, [LtLevel β] → Set (Tangle β)
+  ∀ β : Λ, [LtLevel β] → Set (TSet β)
 
 @[ext]
 theorem Extensions.ext {e₁ e₂ : Extensions} (h : ∀ β : Λ, [LtLevel β] → e₁ β = e₂ β) : e₁ = e₂ :=
@@ -269,7 +269,7 @@ theorem ext_zero (t₁ t₂ : Semitangle) (α_zero : IsMin α) (h : t₁.pref.at
   cases α_zero.not_lt (show β < α from WithBot.coe_lt_coe.mp LtLevel.elim)
 
 /-- Construct a semitangle from an even code. -/
-def intro {β : TypeIndex} [inst : LtLevel β] (s : Set (Tangle β))
+def intro {β : TypeIndex} [inst : LtLevel β] (s : Set (TSet β))
     (heven : (Code.mk β s).IsEven) : Semitangle :=
   ⟨extension s,
     match β, inst, s, heven with
@@ -285,7 +285,7 @@ def intro {β : TypeIndex} [inst : LtLevel β] (s : Set (Tangle β))
           exact congr_arg _ (extension_self s)⟩
 
 @[simp]
-theorem exts_intro (s : Set (Tangle β)) (heven : IsEven (Code.mk β s)) :
+theorem exts_intro (s : Set (TSet β)) (heven : IsEven (Code.mk β s)) :
     (intro s heven).members = extension s :=
   rfl
 
@@ -304,7 +304,7 @@ We now establish that allowable permutations can act on semitangles.
 variable {ρ : NewAllowable} {e : Extensions}
 
 @[simp]
-theorem smul_extension_apply (ρ : NewAllowable) (s : Set (Tangle β)) :
+theorem smul_extension_apply (ρ : NewAllowable) (s : Set (TSet β)) :
     ρ.val γ • extension s γ = extension (ρ.val β • s) γ := by
   by_cases h : β = γ
   · subst h
@@ -324,14 +324,14 @@ instance : MulAction SemiallowablePerm Extensions
     simp only [SemiallowablePerm.mul_apply, mul_smul]
 
 @[simp]
-theorem smul_extension (ρ : NewAllowable) (s : Set (Tangle β)) :
+theorem smul_extension (ρ : NewAllowable) (s : Set (TSet β)) :
     ρ • extension s = extension (ρ.val β • s) := by
   ext γ : 2
   rw [← smul_extension_apply]
   rfl
 
-theorem smul_aux₁ {s : Set (Tangle ⊥)}
-    (h : ∀ γ : Λ, [LtLevel γ] → cloud bot_ne_coe s = (e γ : Set (Tangle γ))) (γ : Λ) [LtLevel γ] :
+theorem smul_aux₁ {s : Set (TSet ⊥)}
+    (h : ∀ γ : Λ, [LtLevel γ] → cloud bot_ne_coe s = (e γ : Set (TSet γ))) (γ : Λ) [LtLevel γ] :
     cloud bot_ne_coe (ρ.val ⊥ • s) = (ρ • e) γ := by
   have := congr_arg (fun c => ρ.val γ • c) (h γ)
   dsimp only at this
@@ -340,7 +340,7 @@ theorem smul_aux₁ {s : Set (Tangle ⊥)}
 
 theorem smul_aux₂
     (h : ∀ (δ : Λ) [LtLevel δ] (hγδ : (γ : TypeIndex) ≠ δ),
-      cloud hγδ (e γ) = (e δ : Set (Tangle δ)))
+      cloud hγδ (e γ) = (e δ : Set (TSet δ)))
     (δ : Λ) [LtLevel δ] (hγδ : (γ : TypeIndex) ≠ δ) : cloud hγδ ((ρ • e) γ) = (ρ • e) δ := by
   have := congr_arg (fun c => ρ.val δ • c) (h δ hγδ)
   dsimp only at this
@@ -429,7 +429,7 @@ theorem Code.Equiv.supported_iff (hcd : c ≡ d) :
   · exact ⟨S, hcd.symm.supports hS⟩
 
 @[simp]
-theorem smul_intro {β : TypeIndex} [inst : LtLevel β]  (ρ : NewAllowable) (s : Set (Tangle β)) (hs) :
+theorem smul_intro {β : TypeIndex} [inst : LtLevel β]  (ρ : NewAllowable) (s : Set (TSet β)) (hs) :
     ρ • intro s hs = intro (ρ.val β • s) (isEven_smul.mpr hs) := by
   induction β using WithBot.recBotCoe generalizing inst
   · simp only [intro, NewAllowable.smul_base, Semitangle.mk.injEq, NewAllowable.smul_extension,
@@ -461,7 +461,7 @@ theorem NewAllowable.smul_address_eq_smul_iff
 /-- For any atom `a`, the code `(α, ⊥, a)` is a tangle at level `α`.
 This is called a *typed atom*. -/
 def newTypedAtom (a : Atom) : NewTangle :=
-  ⟨intro (show Set (Tangle ⊥) from {a}) <| Code.isEven_bot _,
+  ⟨intro (show Set (TSet ⊥) from {a}) <| Code.isEven_bot _,
     ⟨1, fun _ _ => ⟨Quiver.Hom.toPath (bot_lt_coe _), Sum.inl a⟩⟩,
     by
       intro ρ h
@@ -475,7 +475,7 @@ def newTypedAtom (a : Atom) : NewTangle :=
 /-- For any near-litter `N`, the code `(α, ⊥, N)` is a tangle at level `α`.
 This is called a *typed near litter*. -/
 def newTypedNearLitter (N : NearLitter) : NewTangle :=
-  ⟨intro (show Set (Tangle ⊥) from N.2.1) <| Code.isEven_bot _,
+  ⟨intro (show Set (TSet ⊥) from N.2.1) <| Code.isEven_bot _,
     ⟨1, fun _ _ => ⟨Quiver.Hom.toPath (bot_lt_coe _), Sum.inr N⟩⟩,
     by
       intro ρ h