diff --git a/Cslib.lean b/Cslib.lean
index 982b94f5d..c40729499 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -70,9 +70,6 @@ public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
 public import Cslib.Foundations.Data.BiTape
-public import Cslib.Foundations.Data.DecidableEqZero
-public import Cslib.Foundations.Data.FinFun.Basic
-public import Cslib.Foundations.Data.FinFun.Update
 public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Data.Nat.Segment
 public import Cslib.Foundations.Data.OmegaSequence.Defs
diff --git a/Cslib/Foundations/Data/DecidableEqZero.lean b/Cslib/Foundations/Data/DecidableEqZero.lean
deleted file mode 100644
index 0e76e4c68..000000000
--- a/Cslib/Foundations/Data/DecidableEqZero.lean
+++ /dev/null
@@ -1,20 +0,0 @@
-/-
-Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
--/
-
-module
-
-public import Cslib.Init
-
-/-! -/
-
-@[expose] public section
-
-namespace Cslib
-
-/-- Equality to `Zero` is decidable for all elements of a type (`α`). -/
-abbrev DecidableEqZero (α : Type*) [Zero α] := ∀ a : α, Decidable (a = 0)
-
-end Cslib
diff --git a/Cslib/Foundations/Data/FinFun/Basic.lean b/Cslib/Foundations/Data/FinFun/Basic.lean
deleted file mode 100644
index 652b3d123..000000000
--- a/Cslib/Foundations/Data/FinFun/Basic.lean
+++ /dev/null
@@ -1,145 +0,0 @@
-/-
-Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi, Xueying Qin
--/
-
-module
-
-public import Cslib.Init
-public import Mathlib.Data.Finset.Filter
-public import Mathlib.Data.Finset.Lattice.Basic
-
-/-! # Finite functions
-
-Given types `α` and `β`, and assuming that `β` has a `Zero` element,
-a `FinFun α β` is a function from `α` to `β` where only a finite number of elements
-in `α` are mapped to non-zero elements.
--/
-
-@[expose] public section
-
-namespace Cslib
-
-/-- A `FinFun` is a function `fn` with a finite `support`.
-
-This is similar to `Finsupp` in Mathlib, but definitions are computable. -/
-structure FinFun (α β : Type*) [Zero β] where
-  /-- The underlying function. -/
-  fn : α → β
-  /-- The finite support of the function. -/
-  support : Finset α
-  /-- Proof that `support` is the support of the underlying function. -/
-  mem_support_fn {a : α} : a ∈ support ↔ fn a ≠ 0
-
-attribute [scoped grind _=_] FinFun.mem_support_fn
-
-namespace FinFun
-
-@[inherit_doc]
-scoped infixr:25 " →₀ " => FinFun
-
-/-- Constructs a `FinFun` by restricting a function to a given support, filtering out all elements
-not mapped to 0 in the support. -/
-@[scoped grind .]
-def fromFun {α β : Type*} [Zero β] [DecidableEq α]
-  [∀ y : β, Decidable (y = 0)] (fn : α → β) (support : Finset α) : α →₀ β where
-  fn := (fun a => if a ∈ support then fn a else 0)
-  support := support.filter (fn · ≠ 0)
-  mem_support_fn := by grind
-
-@[inherit_doc]
-scoped notation f:25 "↾₀" support:51 => FinFun.fromFun f support
-
-instance instFunLike [Zero β] : FunLike (α →₀ β) α β where
-  coe f := f.fn
-  coe_injective := by
-    rintro ⟨_, _⟩ ⟨_, _⟩
-    simp_all [Finset.ext_iff]
-
-@[scoped grind =]
-theorem coe_fn [Zero β] {f : α →₀ β} : (f : α → β) = f.fn := by simp [DFunLike.coe]
-
-@[scoped grind =]
-theorem coe_eq_fn [Zero β] {f : α →₀ β} : f a = f.fn a := by
-  simp [DFunLike.coe]
-
-/-- Extensional equality for `FinFun`. -/
-@[scoped grind ←=]
-theorem ext [Zero β] {f g : α →₀ β} (h : ∀ (a : α), f a = g a) : f = g :=
-  DFunLike.ext (f := f) (g := g) h
-
-@[scoped grind _=_]
-theorem mem_support_not_zero [Zero β] {f : α →₀ β} : a ∈ f.support ↔ f a ≠ 0 := by
-  grind
-
-@[scoped grind _=_]
-theorem not_mem_support_zero [Zero β] {f : α →₀ β} : a ∉ f.support ↔ f a = 0 := by
-  grind
-
-/-- If two `FinFun`s are equal, their underlying functions and supports are equal. -/
-@[scoped grind .]
-theorem eq_fields_eq [Zero β] {f g : α →₀ β} : f = g → f.fn = g.fn ∧ f.support = g.support :=
-  by grind
-
-/-- If two functions are equal, two `FinFun`s respectively using them as underlying functions
-are equal. -/
-@[scoped grind .]
-theorem fn_eq_eq [Zero β] {f g : α →₀ β} (h : f.fn = g.fn) : f = g :=
-  ext (congrFun h)
-
-@[scoped grind =>]
-theorem congrFinFun [Zero β] {f g : α →₀ β} (h : f = g) (a : α) : f a = g a := by grind
-
-@[scoped grind =]
-theorem fromFun_eq [Zero β] [DecidableEq α] [∀ y : β, Decidable (y = 0)]
-    (f : α → β) (support : Finset α) (h : ∀ a, a ∉ support → f a = 0) :
-    (f ↾₀ support) = f := by grind
-
-@[scoped grind =]
-theorem fromFun_fn [Zero β] [DecidableEq α] [∀ y : β, Decidable (y = 0)]
-    (f : α → β) (support : Finset α) :
-    (f ↾₀ support).fn = (fun a => if a ∈ support then f a else 0) := by
-  grind
-
-@[scoped grind =]
-theorem fromFun_support [Zero β] [DecidableEq α] [∀ y : β, Decidable (y = 0)]
-    (f : α → β) (support : Finset α) :
-    (f ↾₀ support).support = support.filter (f · ≠ 0) := by
-  grind
-
-/-- Restricting a function twice to the same support is idempotent. -/
-@[scoped grind =]
-theorem fromFun_idem [Zero β] [DecidableEq α]
-    [∀ y : β, Decidable (y = 0)] {f : α → β} {support : Finset α} :
-    (f ↾₀ support) ↾₀ support = f ↾₀ support := by grind
-
-/-- Restricting a `FinFun` to its own support is the identity. -/
-@[scoped grind =]
-theorem coe_fromFun_id [Zero β] [DecidableEq α] [∀ y : β, Decidable (y = 0)] {f : α →₀ β} :
-    (f ↾₀ f.support) = f := by grind
-
-/-- Restricting a function twice to two supports is equal to restricting to their intersection. -/
-@[scoped grind =]
-theorem fromFun_inter [Zero β] [DecidableEq α]
-    [∀ y : β, Decidable (y = 0)] {f : α → β} {support1 support2 : Finset α} :
-    (f ↾₀ support1) ↾₀ support2 = f ↾₀ (support1 ∩ support2) := by grind
-
-/-- Restricting a function is commutative. -/
-@[scoped grind =]
-theorem fromFun_comm [Zero β] [DecidableEq α]
-    [∀ y : β, Decidable (y = 0)] {f : α → β} {support1 support2 : Finset α} :
-    (f ↾₀ support1) ↾₀ support2 = (f ↾₀ support2) ↾₀ support1 := by
-  grind only [= coe_eq_fn, = fromFun_fn, ←= ext]
-
-/-- Decidable equality -/
-instance instDecidableEq [Zero β] [DecidableEq α] [DecidableEq β] : DecidableEq (α →₀ β) :=
-  fun f g =>
-    if h : ∀ a ∈ f.support ∪ g.support, f a = g a then
-      isTrue <| ext fun a => by grind
-    else
-      isFalse <| by grind
-
-end FinFun
-
-end Cslib
diff --git a/Cslib/Foundations/Data/FinFun/Update.lean b/Cslib/Foundations/Data/FinFun/Update.lean
deleted file mode 100644
index d02941e77..000000000
--- a/Cslib/Foundations/Data/FinFun/Update.lean
+++ /dev/null
@@ -1,68 +0,0 @@
-/-
-Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
--/
-
-module
-
-public import Cslib.Foundations.Data.FinFun.Basic
-public import Cslib.Foundations.Data.DecidableEqZero
-public import Mathlib.Data.Finset.SDiff
-
-/-! # Update for finite functions
-
-This module defines the update operation for finite functions, that is, the equivalent of
-`Function.update` for `FinFun`.
--/
-
-@[expose] public section
-
-namespace Cslib.FinFun
-
-variable [Zero β] [DecidableEq α] [DecidableEqZero β]
-
-set_option linter.tacticAnalysis.verifyGrindOnly false in
-/-- `FinFun` equivalent of `Function.update`. -/
-def update (f : α →₀ β) (a : α) (b : β) : α →₀ β where
-  fn := Function.update f.fn a b
-  support := if b = 0 then f.support \ {a} else f.support ∪ {a}
-  mem_support_fn := by
-    by_cases b = 0
-    · grind only [= Finset.mem_sdiff, = Finset.mem_singleton, = Function.update, = mem_support_fn]
-    · grind
-
-/-- `FinFun.update` is consistent with `Function.update`. -/
-@[scoped grind =, simp]
-theorem update_coe (f : α →₀ β) : (f.update a b : α → β) = Function.update f a b := by
-  grind [update]
-
-/-- Conditional characterisation of the functional interface of `FinFun.update`. -/
-@[scoped grind =]
-theorem update_apply (f : α →₀ β) : ((f.update a' b) a) = if a = a' then b else f a := by
-  simp [Function.update_apply]
-
-/-- Conditional characterisation of the support of an updated `FinFun`. -/
-@[scoped grind =]
-theorem update_support (f : α →₀ β) :
-    (f.update a b).support = if b = 0 then f.support \ {a} else f.support ∪ {a} := by simp [update]
-
-/-- Updating a finite function on the same key is the same as doing the last update. -/
-@[scoped grind =, simp]
-theorem update_idem (f : α →₀ β) : (f.update a b).update a b' = f.update a b' := by grind
-
-/-- Updates on different keys commute. -/
-@[scoped grind =]
-theorem update_comm (f : α →₀ β) (h : a ≠ a') :
-    (f.update a b).update a' b' = (f.update a' b').update a b := by
-  grind only [←= ext, = update_apply]
-
-/-- Updates that do not change mappings are redundant. -/
-@[scoped grind =]
-theorem update_self (f : α →₀ β) : (f.update a (f a)) = f := by grind
-
-/-- Updating a function never grows its support more than adding the key. -/
-@[scoped grind .]
-theorem update_support_subseteq (f : α →₀ β) : (f.update a b).support ⊆ f.support ∪ {a} := by grind
-
-end Cslib.FinFun
diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean
index 70cce89a0..b650da2b6 100644
--- a/CslibTests/GrindLint.lean
+++ b/CslibTests/GrindLint.lean
@@ -28,11 +28,6 @@ open_scoped_all Cslib
 
 #grind_lint skip Cslib.LTS.Bisimilarity.trans
 #grind_lint skip Cslib.FLTS.toLTS_tr
-#grind_lint skip Cslib.FinFun.coe_fromFun_id
-#grind_lint skip Cslib.FinFun.fromFun_comm
-#grind_lint skip Cslib.FinFun.fromFun_eq
-#grind_lint skip Cslib.FinFun.fromFun_idem
-#grind_lint skip Cslib.FinFun.fromFun_inter
 #grind_lint skip Cslib.LTS.DeterministicStateLabel.not_tr_of_ne
 #grind_lint skip Cslib.LTS.DeterministicStateLabel.image_singleton_iff_tr
 #grind_lint skip Cslib.LTS.Execution.refl