From a1bbc324574fb9e298b08ebfc1d02735a9c3973a Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Tue, 22 Jul 2025 17:05:04 +0200
Subject: [PATCH 1/2] Switch to the standard type for relations.

---
 Cslib/Data/Relation.lean | 103 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 103 insertions(+)
 create mode 100644 Cslib/Data/Relation.lean

diff --git a/Cslib/Data/Relation.lean b/Cslib/Data/Relation.lean
new file mode 100644
index 00000000..6ca9b30d
--- /dev/null
+++ b/Cslib/Data/Relation.lean
@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi and Thomas Waring. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi, Thomas Waring, Chris Henson
+-/
+
+import Mathlib.Logic.Relation
+
+/-! # Relations -/
+
+universe u v
+
+section Relation
+
+/-- Union of two relations. -/
+def Relation.union (r s : α → β → Prop) : α → β → Prop :=
+  fun x y => r x y ∨ s x y
+
+instance {α : Type u} {β : Type v} : Union (α → β → Prop) where
+  union := Relation.union
+
+/-- Inverse of a relation. -/
+def Relation.inv (r : α → β → Prop) : β → α → Prop := flip r
+
+-- /-- Composition of two relations. -/
+-- def Relation.comp (r : α → β → Prop) (s : β → γ → Prop) : α → γ → Prop :=
+--   fun x z => ∃ y, r x y ∧ s y z
+
+/-- The relation `r` 'up to' the relation `s`. -/
+def Relation.upTo (r s : α → α → Prop) : α → α → Prop := Relation.Comp s (Relation.Comp r s)
+
+/-- The identity relation. -/
+inductive Relation.Id : α → α → Prop where
+| id {x : α} : Id x x
+
+/-- A relation has the diamond property when all reductions with a common origin are joinable -/
+abbrev Diamond (R : α → α → Prop) := ∀ {A B C : α}, R A B → R A C → (∃ D, R B D ∧ R C D)
+
+/-- A relation is confluent when its reflexive transitive closure has the diamond property. -/
+abbrev Confluence (R : α → α → Prop) := Diamond (Relation.ReflTransGen R)
+
+/-- Extending a multistep reduction by a single step preserves multi-joinability. -/
+lemma Relation.ReflTransGen.diamond_extend (h : Diamond R) :
+  Relation.ReflTransGen R A B →
+  R A C →
+  ∃ D, Relation.ReflTransGen R B D ∧ Relation.ReflTransGen R C D := by
+  intros AB _
+  revert C
+  induction AB using Relation.ReflTransGen.head_induction_on <;> intros C AC
+  case refl => exact ⟨C, ⟨single AC, by rfl⟩⟩
+  case head A'_C' _ ih =>
+    obtain ⟨D, ⟨CD, C'_D⟩⟩ := h AC A'_C'
+    obtain ⟨D', ⟨B_D', D_D'⟩⟩ := ih C'_D
+    exact ⟨D', ⟨B_D', head CD D_D'⟩⟩
+
+/-- The diamond property implies confluence. -/
+theorem Relation.ReflTransGen.diamond_confluence (h : Diamond R) : Confluence R := by
+  intros A B C AB BC
+  revert C
+  induction AB using Relation.ReflTransGen.head_induction_on <;> intros C BC
+  case refl => exists C
+  case head _ _ A'_C' _ ih =>
+    obtain ⟨D, ⟨CD, C'_D⟩⟩ := diamond_extend h BC A'_C'
+    obtain ⟨D', ⟨B_D', D_D'⟩⟩ := ih C'_D
+    exact ⟨D', ⟨B_D', trans CD D_D'⟩⟩
+
+-- not sure why this doesn't compile as an "instance" but oh well
+def trans_of_subrelation {α : Type _} (s s' r : α → α → Prop) (hr : Transitive r)
+    (h : ∀ a b : α, s a b → r a b) (h' : ∀ a b : α, s' a b → r a b) : Trans s s' r where
+  trans := by
+    intro a b c hab hbc
+    replace hab := h _ _ hab
+    replace hbc := h' _ _ hbc
+    exact hr hab hbc
+
+def trans_of_subrelation_left {α : Type _} (s r : α → α → Prop) (hr : Transitive r)
+    (h : ∀ a b : α, s a b → r a b) : Trans s r r where
+  trans := by
+    intro a b c hab hbc
+    replace hab := h _ _ hab
+    exact hr hab hbc
+
+def trans_of_subrelation_right {α : Type _} (s r : α → α → Prop) (hr : Transitive r)
+    (h : ∀ a b : α, s a b → r a b) : Trans r s r where
+  trans := by
+    intro a b c hab hbc
+    replace hbc := h _ _ hbc
+    exact hr hab hbc
+
+/-- This is a straightforward but useful specialisation of a more general result in
+`Mathlib.Logic.Relation`. -/
+theorem church_rosser_of_diamond {α : Type _} {r : α → α → Prop}
+    (h : ∀ a b c, r a b → r a c → Relation.Join r b c) :
+    Equivalence (Relation.Join (Relation.ReflTransGen r)) := by
+  apply Relation.equivalence_join_reflTransGen
+  intro a b c hab hac
+  let ⟨d, hd⟩ := h a b c hab hac
+  use d
+  constructor
+  . exact Relation.ReflGen.single hd.1
+  . exact Relation.ReflTransGen.single hd.2
+
+end Relation

From 18f8b43f9baeb05c8057481cf87e43283e07de30 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Tue, 22 Jul 2025 17:15:50 +0200
Subject: [PATCH 2/2] Missing changes

---
 Cslib.lean                                    |   2 +-
 .../CombinatoryLogic/Confluence.lean          |   2 +-
 .../Computability/CombinatoryLogic/Defs.lean  |   2 +-
 .../LocallyNameless/FullBetaConfluence.lean   |   2 +-
 .../CCS/BehaviouralTheory.lean                |  16 +--
 Cslib/ConcurrencyTheory/CCS/Semantics.lean    |   5 +-
 Cslib/Semantics/LTS/Basic.lean                |  14 +-
 Cslib/Semantics/LTS/Bisimulation.lean         | 127 +++++++++---------
 Cslib/Semantics/LTS/Simulation.lean           |  32 ++---
 Cslib/Utils/Rel.lean                          |  18 ---
 Cslib/Utils/Relation.lean                     |  77 -----------
 CslibTests/Bisimulation.lean                  |   2 +-
 CslibTests/LTS.lean                           |   2 +-
 13 files changed, 104 insertions(+), 197 deletions(-)
 delete mode 100644 Cslib/Utils/Rel.lean
 delete mode 100644 Cslib/Utils/Relation.lean

diff --git a/Cslib.lean b/Cslib.lean
index 9ed21b31..aa2a1c43 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,6 +1,6 @@
 import Cslib.Semantics.LTS.Basic
 import Cslib.Semantics.LTS.Bisimulation
 import Cslib.Semantics.LTS.TraceEq
-import Cslib.Utils.Relation
+import Cslib.Data.Relation
 import Cslib.Computability.CombinatoryLogic.Defs
 import Cslib.Computability.CombinatoryLogic.Basic
diff --git a/Cslib/Computability/CombinatoryLogic/Confluence.lean b/Cslib/Computability/CombinatoryLogic/Confluence.lean
index 5c0fb508..94da8ab3 100644
--- a/Cslib/Computability/CombinatoryLogic/Confluence.lean
+++ b/Cslib/Computability/CombinatoryLogic/Confluence.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Waring
 -/
 import Cslib.Computability.CombinatoryLogic.Defs
-import Cslib.Utils.Relation
+import Cslib.Data.Relation
 
 /-!
 # SKI reduction is confluent
diff --git a/Cslib/Computability/CombinatoryLogic/Defs.lean b/Cslib/Computability/CombinatoryLogic/Defs.lean
index c0b993db..e0bdfe6a 100644
--- a/Cslib/Computability/CombinatoryLogic/Defs.lean
+++ b/Cslib/Computability/CombinatoryLogic/Defs.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Waring
 -/
 import Mathlib.Logic.Relation
-import Cslib.Utils.Relation
+import Cslib.Data.Relation
 
 /-!
 # SKI Combinatory Logic
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
index 5dfc85ba..9c64387c 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
@@ -7,7 +7,7 @@ Authors: Chris Henson
 import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
 import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
 import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.FullBeta
-import Cslib.Utils.Relation
+import Cslib.Data.Relation
 
 /-! # β-confluence for the λ-calculus -/
 
diff --git a/Cslib/ConcurrencyTheory/CCS/BehaviouralTheory.lean b/Cslib/ConcurrencyTheory/CCS/BehaviouralTheory.lean
index df3c1707..35189c24 100644
--- a/Cslib/ConcurrencyTheory/CCS/BehaviouralTheory.lean
+++ b/Cslib/ConcurrencyTheory/CCS/BehaviouralTheory.lean
@@ -23,13 +23,13 @@ Additionally, some standard laws of bisimilarity for CCS, including:
 
 section CCS.BehaviouralTheory
 
-variable {Name : Type u} {Constant : Type v} {defs : Rel Constant (CCS.Process Name Constant)}
+variable {Name : Type u} {Constant : Type v} {defs : Constant → (CCS.Process Name Constant) → Prop}
 
 open CCS CCS.Process CCS.Act
 
 namespace CCS
 
-private inductive ParNil : Rel (Process Name Constant) (Process Name Constant) where
+private inductive ParNil : (Process Name Constant) → (Process Name Constant) → Prop where
 | parNil : ParNil (par p nil) p
 
 /-- P | 𝟎 ~ P -/
@@ -60,7 +60,7 @@ theorem bisimilarity_par_nil (p : Process Name Constant) : (par p nil) ~[@lts Na
     case right =>
       constructor
 
-private inductive ParComm : Rel (Process Name Constant) (Process Name Constant) where
+private inductive ParComm : (Process Name Constant) → (Process Name Constant) → Prop where
 | parComm : ParComm (par p q) (par q p)
 
 /-- P | Q ~ Q | P -/
@@ -114,7 +114,7 @@ theorem bisimilarity_par_comm (p q : Process Name Constant) : (par p q) ~[@lts N
             apply Tr.com htrq htrp
           . constructor
 
-private inductive ChoiceComm : Rel (Process Name Constant) (Process Name Constant) where
+private inductive ChoiceComm : (Process Name Constant) → (Process Name Constant) → Prop where
 | choiceComm : ChoiceComm (choice p q) (choice q p)
 | bisim : (p ~[@lts Name Constant defs] q) → ChoiceComm p q
 
@@ -166,7 +166,7 @@ theorem bisimilarity_choice_comm : (choice p q) ~[@lts Name Constant defs] (choi
       apply And.intro htr1
       constructor; assumption
 
-private inductive PreBisim : Rel (Process Name Constant) (Process Name Constant) where
+private inductive PreBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | pre : (p ~[@lts Name Constant defs] q) → PreBisim (pre μ p) (pre μ q)
 | bisim : (p ~[@lts Name Constant defs] q) → PreBisim p q
 
@@ -217,7 +217,7 @@ theorem bisimilarity_congr_pre : (p ~[@lts Name Constant defs] q) → (pre μ p)
       constructor
       apply Bisimilarity.largest_bisimulation _ r hbisim s1' s2' hr1
 
-private inductive ResBisim : Rel (Process Name Constant) (Process Name Constant) where
+private inductive ResBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | res : (p ~[@lts Name Constant defs] q) → ResBisim (res a p) (res a q)
 -- | bisim : (p ~[@lts Name Constant defs] q) → ResBisim p q
 
@@ -250,7 +250,7 @@ theorem bisimilarity_congr_res : (p ~[@lts Name Constant defs] q) → (res a p)
     constructor; constructor; repeat assumption
     constructor; assumption
 
-private inductive ChoiceBisim : Rel (Process Name Constant) (Process Name Constant) where
+private inductive ChoiceBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | choice : (p ~[@lts Name Constant defs] q) → ChoiceBisim (choice p r) (choice q r)
 | bisim : (p ~[@lts Name Constant defs] q) → ChoiceBisim p q
 
@@ -315,7 +315,7 @@ theorem bisimilarity_congr_choice : (p ~[@lts Name Constant defs] q) → (choice
       constructor
       apply Bisimilarity.largest_bisimulation _ _ hb _ _ hr1
 
-private inductive ParBisim : Rel (Process Name Constant) (Process Name Constant) where
+private inductive ParBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | par : (p ~[@lts Name Constant defs] q) → ParBisim (par p r) (par q r)
 
 /-- P ~ Q → P | R ~ Q | R-/
diff --git a/Cslib/ConcurrencyTheory/CCS/Semantics.lean b/Cslib/ConcurrencyTheory/CCS/Semantics.lean
index 1292edd3..04bec2d5 100644
--- a/Cslib/ConcurrencyTheory/CCS/Semantics.lean
+++ b/Cslib/ConcurrencyTheory/CCS/Semantics.lean
@@ -15,7 +15,10 @@ import Cslib.ConcurrencyTheory.CCS.Basic
 
 -/
 
-variable {Name : Type u} {Constant : Type v} {defs : Rel Constant (CCS.Process Name Constant)}
+variable
+  {Name : Type u}
+  {Constant : Type v}
+  {defs : Constant → (CCS.Process Name Constant) → Prop}
 
 namespace CCS
 
diff --git a/Cslib/Semantics/LTS/Basic.lean b/Cslib/Semantics/LTS/Basic.lean
index 4d379793..2b473edb 100644
--- a/Cslib/Semantics/LTS/Basic.lean
+++ b/Cslib/Semantics/LTS/Basic.lean
@@ -7,7 +7,6 @@ Authors: Fabrizio Montesi
 import Mathlib.Tactic.Lemma
 import Mathlib.Data.Finite.Defs
 import Mathlib.Data.Fintype.Basic
-import Mathlib.Data.Rel
 import Mathlib.Logic.Function.Defs
 import Mathlib.Data.Set.Finite.Basic
 import Mathlib.Data.Stream.Defs
@@ -64,11 +63,12 @@ section Relation
 and `s2` such that `lts.Tr s1 μ s2`.
 
 This can be useful, for example, to see a reduction relation as an LTS. -/
-def LTS.toRel (lts : LTS State Label) (μ : Label) : Rel State State :=
+def LTS.toRelation (lts : LTS State Label) (μ : Label) : State → State → Prop :=
   fun s1 s2 => lts.Tr s1 μ s2
 
 /-- Any homogeneous relation can be seen as an LTS where all transitions have the same label. -/
-def Rel.toLTS [DecidableEq Label] (r : Rel State State) (μ : Label) : LTS State Label where
+def Relation.toLTS [DecidableEq Label] (r : State → State → Prop) (μ : Label) :
+  LTS State Label where
   Tr := fun s1 μ' s2 => if μ' = μ then r s1 s2 else False
 
 end Relation
@@ -576,9 +576,9 @@ elab "create_lts" lt:ident name:ident : command => do
       addTermInfo' name (.const name.getId params) (isBinder := true)
       addDeclarationRangesFromSyntax name.getId name
 
-/-- 
+/--
   This command adds notations for an `LTS.Tr`. This should not usually be called directly, but from
-  the `lts` attribute. 
+  the `lts` attribute.
 
   As an example `lts_reduction_notation foo "β"` will add the notations "[⬝]⭢β" and "[⬝]↠β"
 
@@ -588,12 +588,12 @@ elab "create_lts" lt:ident name:ident : command => do
 -/
 syntax "lts_reduction_notation" ident (Lean.Parser.Command.notationItem)? : command
 macro_rules
-  | `(lts_reduction_notation $lts $sym) => 
+  | `(lts_reduction_notation $lts $sym) =>
     `(
       notation:39 t "["μ"]⭢"$sym t' => (LTS.Tr $lts) t μ t'
       notation:39 t "["μ"]↠"$sym t' => (LTS.MTr $lts) t μ t'
      )
-  | `(lts_reduction_notation $lts) => 
+  | `(lts_reduction_notation $lts) =>
     `(
       notation:39 t "["μ"]⭢" t' => (LTS.Tr $lts) t μ t'
       notation:39 t "["μ"]↠" t' => (LTS.MTr $lts) t μ t'
diff --git a/Cslib/Semantics/LTS/Bisimulation.lean b/Cslib/Semantics/LTS/Bisimulation.lean
index 9dd0546a..d529eddb 100644
--- a/Cslib/Semantics/LTS/Bisimulation.lean
+++ b/Cslib/Semantics/LTS/Bisimulation.lean
@@ -6,8 +6,7 @@ Authors: Fabrizio Montesi
 
 import Cslib.Semantics.LTS.Basic
 import Cslib.Semantics.LTS.TraceEq
-import Mathlib.Data.Rel
-import Cslib.Utils.Rel
+import Cslib.Data.Relation
 import Cslib.Semantics.LTS.Simulation
 
 /-! # Bisimulation and Bisimilarity
@@ -73,7 +72,7 @@ variable {State : Type u} {Label : Type v} (lts : LTS State Label)
 /-- A relation is a bisimulation if, whenever it relates two states in an lts,
 the transitions originating from these states mimic each other and the reached
 derivatives are themselves related. -/
-def Bisimulation (lts : LTS State Label) (r : Rel State State) : Prop :=
+def Bisimulation (lts : LTS State Label) (r : State → State → Prop) : Prop :=
   ∀ s1 s2, r s1 s2 → ∀ μ, (
     (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2')
     ∧
@@ -81,17 +80,17 @@ def Bisimulation (lts : LTS State Label) (r : Rel State State) : Prop :=
   )
 
 /-- Helper for following a transition using the first component of a `Bisimulation`. -/
-def Bisimulation.follow_fst {lts : LTS State Label} {r : Rel State State} (hb : Bisimulation lts r) (hr : r s1 s2) (μ : Label) (htr : lts.Tr s1 μ s1'):=
+def Bisimulation.follow_fst {lts : LTS State Label} {r : State → State → Prop} (hb : Bisimulation lts r) (hr : r s1 s2) (μ : Label) (htr : lts.Tr s1 μ s1'):=
   (hb _ _ hr μ).1 _ htr
 
 /-- Helper for following a transition using the second component of a `Bisimulation`. -/
-def Bisimulation.follow_snd {lts : LTS State Label} {r : Rel State State} (hb : Bisimulation lts r) (hr : r s1 s2) (μ : Label) (htr : lts.Tr s2 μ s2'):=
+def Bisimulation.follow_snd {lts : LTS State Label} {r : State → State → Prop} (hb : Bisimulation lts r) (hr : r s1 s2) (μ : Label) (htr : lts.Tr s2 μ s2'):=
   (hb _ _ hr μ).2 _ htr
 
 /-- Two states are bisimilar if they are related by some bisimulation. -/
-def Bisimilarity (lts : LTS State Label) : Rel State State :=
+def Bisimilarity (lts : LTS State Label) : State → State → Prop :=
   fun s1 s2 =>
-    ∃ r : Rel State State, r s1 s2 ∧ Bisimulation lts r
+    ∃ r : State → State → Prop, r s1 s2 ∧ Bisimulation lts r
 
 /--
 Notation for bisimilarity.
@@ -103,7 +102,7 @@ notation s:max " ~[" lts "] " s':max => Bisimilarity lts s s'
 
 /-- Bisimilarity is reflexive. -/
 theorem Bisimilarity.refl (s : State) : s ~[lts] s := by
-  exists Rel.Id
+  exists Relation.Id
   constructor
   case left =>
     constructor
@@ -126,8 +125,8 @@ theorem Bisimilarity.refl (s : State) : s ~[lts] s := by
       · constructor
 
 /-- The inverse of a bisimulation is a bisimulation. -/
-theorem Bisimulation.inv (r : Rel State State) (h : Bisimulation lts r) :
-  Bisimulation lts r.inv := by
+theorem Bisimulation.inv (r : State → State → Prop) (h : Bisimulation lts r) :
+  Bisimulation lts (Relation.inv r) := by
   simp only [Bisimulation] at h
   simp only [Bisimulation]
   intro s1 s2 hrinv μ
@@ -148,7 +147,7 @@ theorem Bisimulation.inv (r : Rel State State) (h : Bisimulation lts r) :
 /-- Bisimilarity is symmetric. -/
 theorem Bisimilarity.symm {s1 s2 : State} (h : s1 ~[lts] s2) : s2 ~[lts] s1 := by
   obtain ⟨r, hr, hb⟩ := h
-  exists r.inv
+  exists (Relation.inv r)
   constructor
   case left =>
     exact hr
@@ -158,8 +157,8 @@ theorem Bisimilarity.symm {s1 s2 : State} (h : s1 ~[lts] s2) : s2 ~[lts] s1 := b
 
 /-- The composition of two bisimulations is a bisimulation. -/
 theorem Bisimulation.comp
-  (r1 r2 : Rel State State) (h1 : Bisimulation lts r1) (h2 : Bisimulation lts r2) :
-  Bisimulation lts (r1.comp r2) := by
+  (r1 r2 : State → State → Prop) (h1 : Bisimulation lts r1) (h2 : Bisimulation lts r2) :
+  Bisimulation lts (Relation.Comp r1 r2) := by
   simp_all only [Bisimulation]
   intro s1 s2 hrc μ
   constructor
@@ -175,7 +174,7 @@ theorem Bisimulation.comp
     exists s2''
     constructor
     · exact h2'tr
-    · simp [Rel.comp]
+    · simp only [Relation.Comp]
       exists s1''
   case right =>
     intro s2' htr
@@ -189,7 +188,7 @@ theorem Bisimulation.comp
     exists s1''
     constructor
     · exact h1'tr
-    · simp [Rel.comp]
+    · simp only [Relation.Comp]
       exists s2''
 
 /-- Bisimilarity is transitive. -/
@@ -198,10 +197,10 @@ theorem Bisimilarity.trans
   s1 ~[lts] s3 := by
   obtain ⟨r1, hr1, hr1b⟩ := h1
   obtain ⟨r2, hr2, hr2b⟩ := h2
-  exists r1.comp r2
+  exists Relation.Comp r1 r2
   constructor
   case left =>
-    simp only [Rel.comp]
+    simp only [Relation.Comp]
     exists s2
   case right =>
     apply Bisimulation.comp lts r1 r2 hr1b hr2b
@@ -250,31 +249,31 @@ theorem Bisimilarity.is_bisimulation : Bisimulation lts (Bisimilarity lts) := by
 
 /-- Bisimilarity is the largest bisimulation. -/
 theorem Bisimilarity.largest_bisimulation
-  (r : Rel State State) (h : Bisimulation lts r) (s1 s2 : State) :
+  (r : State → State → Prop) (h : Bisimulation lts r) (s1 s2 : State) :
   r s1 s2 → s1 ~[lts] s2 := by
   intro hr
   exists r
 
 /-- The union of bisimilarity with any bisimulation is bisimilarity. -/
-theorem Bisimilarity.gfp (r : Rel State State) (h : Bisimulation lts r) :
-  (Bisimilarity lts).union r = Bisimilarity lts := by
+theorem Bisimilarity.gfp (r : State → State → Prop) (h : Bisimulation lts r) :
+  (Bisimilarity lts) ∪ r = Bisimilarity lts := by
   funext s1 s2
-  simp [Rel.union]
+  simp only [Union.union, Relation.union, eq_iff_iff, or_iff_left_iff_imp]
   apply Bisimilarity.largest_bisimulation lts r h
 
 /-- A relation `r` is a bisimulation up to bisimilarity if, whenever it relates two
 states in an lts, the transitions originating from these states mimic each other and the reached
 derivatives are themselves related by `r` up to bisimilarity. -/
-def BisimulationUpTo (lts : LTS State Label) (r : Rel State State) : Prop :=
+def BisimulationUpTo (lts : LTS State Label) (r : State → State → Prop) : Prop :=
   ∀ s1 s2, r s1 s2 → ∀ μ, (
-    (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ r.upTo (Bisimilarity lts) s1' s2')
+    (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ Relation.upTo r (Bisimilarity lts) s1' s2')
     ∧
-    (∀ s2', lts.Tr s2 μ s2' → ∃ s1', lts.Tr s1 μ s1' ∧ r.upTo (Bisimilarity lts) s1' s2')
+    (∀ s2', lts.Tr s2 μ s2' → ∃ s1', lts.Tr s1 μ s1' ∧ Relation.upTo r (Bisimilarity lts) s1' s2')
   )
 
 /-- Any bisimulation up to bisimilarity is a bisimulation. -/
-theorem Bisimulation.upTo_bisimulation (r : Rel State State) (h : BisimulationUpTo lts r) :
-  Bisimulation lts (r.upTo (Bisimilarity lts)) := by
+theorem Bisimulation.upTo_bisimulation (r : State → State → Prop) (h : BisimulationUpTo lts r) :
+  Bisimulation lts (Relation.upTo r (Bisimilarity lts)) := by
   simp [Bisimulation]
   simp [BisimulationUpTo] at h
   intro s1 s2 hr μ
@@ -297,7 +296,7 @@ theorem Bisimulation.upTo_bisimulation (r : Rel State State) (h : BisimulationUp
       constructor
       · apply Bisimilarity.trans lts (Bisimilarity.largest_bisimulation lts r1 hr1b _ _ hs1b'r)
           hsmidb
-      · simp [Rel.comp]
+      · simp only [Relation.Comp]
         exists smid2
         constructor
         · exact hsmidr
@@ -314,7 +313,7 @@ theorem Bisimulation.upTo_bisimulation (r : Rel State State) (h : BisimulationUp
       exact hs1btr
     case right =>
       obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs1b'r
-      simp [Rel.upTo, Rel.comp]
+      simp only [Relation.upTo, Relation.Comp]
       constructor
       constructor
       · apply Bisimilarity.trans lts (Bisimilarity.largest_bisimulation lts r1 hr1b _ _ _) hsmidb
@@ -329,7 +328,7 @@ theorem Bisimulation.upTo_bisimulation (r : Rel State State) (h : BisimulationUp
 /-- If two states are related by a bisimulation, they can mimic each other's multi-step
 transitions. -/
 theorem Bisimulation.bisim_trace
-  (s1 s2 : State) (r : Rel State State) (hb : Bisimulation lts r) (hr : r s1 s2) :
+  (s1 s2 : State) (r : State → State → Prop) (hb : Bisimulation lts r) (hr : r s1 s2) :
   ∀ μs s1', lts.MTr s1 μs s1' → ∃ s2', lts.MTr s2 μs s2' ∧ r s1' s2' := by
   intro μs
   induction μs generalizing s1 s2
@@ -363,7 +362,7 @@ theorem Bisimulation.bisim_trace
 
 /-- Any bisimulation implies trace equivalence. -/
 theorem Bisimulation.bisim_traceEq
-  (s1 s2 : State) (r : Rel State State) (hb : Bisimulation lts r) (hr : r s1 s2) :
+  (s1 s2 : State) (r : State → State → Prop) (hb : Bisimulation lts r) (hr : r s1 s2) :
   s1 ~tr[lts] s2 := by
   simp [TraceEq, LTS.traces, setOf]
   funext μs
@@ -379,7 +378,7 @@ theorem Bisimulation.bisim_traceEq
     intro h
     obtain ⟨s2', h⟩ := h
     have hinv := @Bisimulation.inv State Label lts r hb
-    obtain ⟨s1', hmtr⟩ := @Bisimulation.bisim_trace State Label lts s2 s1 r.inv hinv hr μs s2' h
+    obtain ⟨s1', hmtr⟩ := @Bisimulation.bisim_trace State Label lts s2 s1 (Relation.inv r) hinv hr μs s2' h
     exists s1'
     exact hmtr.1
 
@@ -738,7 +737,7 @@ theorem Bisimilarity.deterministic_bisim_eq_traceEq
 /-! ### Relation to simulation -/
 
 /-- Any bisimulation is also a simulation. -/
-theorem Bisimulation.is_simulation (lts : LTS State Label) (r : Rel State State) : Bisimulation lts r → Simulation lts r := by
+theorem Bisimulation.is_simulation (lts : LTS State Label) (r : State → State → Prop) : Bisimulation lts r → Simulation lts r := by
   intro h
   simp only [Bisimulation] at h
   simp only [Simulation]
@@ -748,7 +747,7 @@ theorem Bisimulation.is_simulation (lts : LTS State Label) (r : Rel State State)
   apply h1 s1' htr
 
 /-- A relation is a bisimulation iff both it and its inverse are simulations. -/
-theorem Bisimulation.simulation_iff (lts : LTS State Label) (r : Rel State State) : Bisimulation lts r ↔ (Simulation lts r ∧ Simulation lts r.inv) := by
+theorem Bisimulation.simulation_iff (lts : LTS State Label) (r : State → State → Prop) : Bisimulation lts r ↔ (Simulation lts r ∧ Simulation lts (Relation.inv r)) := by
   constructor
   intro h
   simp only [Simulation]
@@ -762,7 +761,7 @@ theorem Bisimulation.simulation_iff (lts : LTS State Label) (r : Rel State State
       obtain ⟨s2', h1⟩ := h1
       exists s2'
     case right =>
-      simp only [Rel.inv, flip]
+      simp only [Relation.inv, flip]
       intro s2 s1 hr μ s2' htr
       simp only [Bisimulation] at h
       specialize h s1 s2 hr μ
@@ -791,13 +790,13 @@ section WeakBisimulation
 
 /-- A weak bisimulation is similar to a `Bisimulation`, but allows for the related processes to do
 internal work. Technically, this is defined as a `Bisimulation` on the saturation of the LTS. -/
-def WeakBisimulation [HasTau Label] (lts : LTS State Label) (r : Rel State State) :=
+def WeakBisimulation [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) :=
   Bisimulation (lts.saturate) r
 
 /-- Two states are weakly bisimilar if they are related by some weak bisimulation. -/
-def WeakBisimilarity [HasTau Label] (lts : LTS State Label) : Rel State State :=
+def WeakBisimilarity [HasTau Label] (lts : LTS State Label) : State → State → Prop :=
   fun s1 s2 =>
-    ∃ r : Rel State State, r s1 s2 ∧ WeakBisimulation lts r
+    ∃ r : State → State → Prop, r s1 s2 ∧ WeakBisimulation lts r
 
 /-- Notation for weak bisimilarity. -/
 notation s:max " ≈[" lts "] " s':max => WeakBisimilarity lts s s'
@@ -805,7 +804,7 @@ notation s:max " ≈[" lts "] " s':max => WeakBisimilarity lts s s'
 /-- An `SWBisimulation` is a more convenient definition of weak bisimulation, because the challenge
 is a single transition. We prove later that this technique is sound, following a strategy inspired
 by [Sangiorgi2011]. -/
-def SWBisimulation [HasTau Label] (lts : LTS State Label) (r : Rel State State) : Prop :=
+def SWBisimulation [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) : Prop :=
   ∀ s1 s2, r s1 s2 → ∀ μ, (
     (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.STr s2 μ s2' ∧ r s1' s2')
     ∧
@@ -813,9 +812,9 @@ def SWBisimulation [HasTau Label] (lts : LTS State Label) (r : Rel State State)
   )
 
 /-- Two states are sw-bisimilar if they are related by some sw-bisimulation. -/
-def SWBisimilarity [HasTau Label] (lts : LTS State Label) : Rel State State :=
+def SWBisimilarity [HasTau Label] (lts : LTS State Label) : State → State → Prop :=
   fun s1 s2 =>
-    ∃ r : Rel State State, r s1 s2 ∧ SWBisimulation lts r
+    ∃ r : State → State → Prop, r s1 s2 ∧ SWBisimulation lts r
 
 /-- Notation for swbisimilarity. -/
 notation s:max " ≈sw[" lts "] " s':max => SWBisimilarity lts s s'
@@ -823,7 +822,7 @@ notation s:max " ≈sw[" lts "] " s':max => SWBisimilarity lts s s'
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (first component, weighted version). -/
 theorem SWBisimulation.follow_internal_fst_n
-  [HasTau Label] (lts : LTS State Label) (r : Rel State State)
+  [HasTau Label] (lts : LTS State Label) (r : State → State → Prop)
   (hswb : SWBisimulation lts r) (hr : r s1 s2) (hstrN : lts.strN n s1 HasTau.τ s1') :
   ∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by
   cases n
@@ -851,7 +850,7 @@ theorem SWBisimulation.follow_internal_fst_n
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (second component, weighted version). -/
 theorem SWBisimulation.follow_internal_snd_n
-  [HasTau Label] (lts : LTS State Label) (r : Rel State State)
+  [HasTau Label] (lts : LTS State Label) (r : State → State → Prop)
   (hswb : SWBisimulation lts r) (hr : r s1 s2) (hstrN : lts.strN n s2 HasTau.τ s2') :
   ∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by
   cases n
@@ -879,7 +878,7 @@ theorem SWBisimulation.follow_internal_snd_n
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (first component). -/
 theorem SWBisimulation.follow_internal_fst
-  [HasTau Label] (lts : LTS State Label) (r : Rel State State)
+  [HasTau Label] (lts : LTS State Label) (r : State → State → Prop)
   (hswb : SWBisimulation lts r) (hr : r s1 s2) (hstr : lts.STr s1 HasTau.τ s1') :
   ∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by
   obtain ⟨n, hstrN⟩ := (LTS.str_strN lts).1 hstr
@@ -888,14 +887,14 @@ theorem SWBisimulation.follow_internal_fst
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (second component). -/
 theorem SWBisimulation.follow_internal_snd
-  [HasTau Label] (lts : LTS State Label) (r : Rel State State)
+  [HasTau Label] (lts : LTS State Label) (r : State → State → Prop)
   (hswb : SWBisimulation lts r) (hr : r s1 s2) (hstr : lts.STr s2 HasTau.τ s2') :
   ∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by
   obtain ⟨n, hstrN⟩ := (LTS.str_strN lts).1 hstr
   apply SWBisimulation.follow_internal_snd_n lts r hswb hr hstrN
 
 /-- We can now prove that any relation is a `WeakBisimulation` iff it is an `SWBisimulation`. This formalises lemma 4.2.10 in [Sangiorgi2011]. -/
-theorem WeakBisimulation.iff_swBisimulation [HasTau Label] (lts : LTS State Label) (r : Rel State State) :
+theorem WeakBisimulation.iff_swBisimulation [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) :
   WeakBisimulation lts r ↔ SWBisimulation lts r := by
   apply Iff.intro
   case mp =>
@@ -954,13 +953,13 @@ theorem WeakBisimulation.iff_swBisimulation [HasTau Label] (lts : LTS State Labe
           apply LTS.STr.comp lts hstr1b hstr1b' hstr1'
         · exact hrb2
 
-theorem WeakBisimulation.toSwBisimulation [HasTau Label] {lts : LTS State Label} {r : Rel State State} (h : WeakBisimulation lts r) : SWBisimulation lts r := (WeakBisimulation.iff_swBisimulation lts r).1 h
+theorem WeakBisimulation.toSwBisimulation [HasTau Label] {lts : LTS State Label} {r : State → State → Prop} (h : WeakBisimulation lts r) : SWBisimulation lts r := (WeakBisimulation.iff_swBisimulation lts r).1 h
 
-theorem SWBisimulation.toWeakBisimulation [HasTau Label] {lts : LTS State Label} {r : Rel State State} (h : SWBisimulation lts r) : WeakBisimulation lts r := (WeakBisimulation.iff_swBisimulation lts r).2 h
+theorem SWBisimulation.toWeakBisimulation [HasTau Label] {lts : LTS State Label} {r : State → State → Prop} (h : SWBisimulation lts r) : WeakBisimulation lts r := (WeakBisimulation.iff_swBisimulation lts r).2 h
 
 /-- If two states are related by an `SWBisimulation`, then they are weakly bisimilar. -/
 theorem WeakBisimilarity.by_swBisimulation [HasTau Label]
-  (lts : LTS State Label) (r : Rel State State)
+  (lts : LTS State Label) (r : State → State → Prop)
   (hb : SWBisimulation lts r) (hr : r s1 s2) : s1 ≈[lts] s2 := by
   exists r
   constructor; exact hr
@@ -988,7 +987,7 @@ theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] (lts : LTS State La
 /-- sw-bisimilarity is reflexive. -/
 theorem SWBisimilarity.refl [HasTau Label] (lts : LTS State Label) (s : State) : s ≈sw[lts] s := by
   simp [SWBisimilarity]
-  exists Rel.Id
+  exists Relation.Id
   constructor; constructor
   simp [SWBisimulation]
   intro s1 s2 hr μ
@@ -1014,8 +1013,8 @@ theorem WeakBisimilarity.refl [HasTau Label] (lts : LTS State Label) (s : State)
 
 /-- The inverse of an sw-bisimulation is an sw-bisimulation. -/
 theorem SWBisimulation.inv [HasTau Label] (lts : LTS State Label)
-  (r : Rel State State) (h : SWBisimulation lts r) :
-  SWBisimulation lts r.inv := by
+  (r : State → State → Prop) (h : SWBisimulation lts r) :
+  SWBisimulation lts (Relation.inv r) := by
   simp only [SWBisimulation] at h
   simp only [SWBisimulation]
   intro s1 s2 hrinv μ
@@ -1035,8 +1034,8 @@ theorem SWBisimulation.inv [HasTau Label] (lts : LTS State Label)
 
 /-- The inverse of a weak bisimulation is a weak bisimulation. -/
 theorem WeakBisimulation.inv [HasTau Label] (lts : LTS State Label)
-  (r : Rel State State) (h : WeakBisimulation lts r) :
-  WeakBisimulation lts r.inv := by
+  (r : State → State → Prop) (h : WeakBisimulation lts r) :
+  WeakBisimulation lts (Relation.inv r) := by
   apply WeakBisimulation.toSwBisimulation at h
   have h' := SWBisimulation.inv lts r h
   apply SWBisimulation.toWeakBisimulation at h'
@@ -1045,10 +1044,10 @@ theorem WeakBisimulation.inv [HasTau Label] (lts : LTS State Label)
 /-- sw-bisimilarity is symmetric. -/
 theorem SWBisimilarity.symm [HasTau Label] (lts : LTS State Label) (h : s1 ≈sw[lts] s2) : s2 ≈sw[lts] s1 := by
   obtain ⟨r, hr, hrh⟩ := h
-  exists r.inv
+  exists (Relation.inv r)
   constructor
   case left =>
-    simp only [Rel.inv, flip]
+    simp only [Relation.inv, flip]
     exact hr
   case right =>
     apply SWBisimulation.inv lts r hrh
@@ -1063,8 +1062,8 @@ theorem WeakBisimilarity.symm [HasTau Label] (lts : LTS State Label) (h : s1 ≈
 theorem WeakBisimulation.comp
   [HasTau Label]
   (lts : LTS State Label)
-  (r1 r2 : Rel State State) (h1 : WeakBisimulation lts r1) (h2 : WeakBisimulation lts r2) :
-  WeakBisimulation lts (r1.comp r2) := by
+  (r1 r2 : State → State → Prop) (h1 : WeakBisimulation lts r1) (h2 : WeakBisimulation lts r2) :
+  WeakBisimulation lts (Relation.Comp r1 r2) := by
   simp_all only [WeakBisimulation]
   intro s1 s2 hrc μ
   constructor
@@ -1080,7 +1079,7 @@ theorem WeakBisimulation.comp
     exists s2''
     constructor
     · exact h2'tr
-    · simp [Rel.comp]
+    · simp only [Relation.Comp]
       exists s1''
   case right =>
     intro s2' htr
@@ -1094,18 +1093,18 @@ theorem WeakBisimulation.comp
     exists s1''
     constructor
     · exact h1'tr
-    · simp [Rel.comp]
+    · simp only [Relation.Comp]
       exists s2''
 
 /-- The composition of two sw-bisimulations is an sw-bisimulation. -/
 theorem SWBisimulation.comp
   [HasTau Label]
   (lts : LTS State Label)
-  (r1 r2 : Rel State State) (h1 : SWBisimulation lts r1) (h2 : SWBisimulation lts r2) :
-  SWBisimulation lts (r1.comp r2) := by
+  (r1 r2 : State → State → Prop) (h1 : SWBisimulation lts r1) (h2 : SWBisimulation lts r2) :
+  SWBisimulation lts (Relation.Comp r1 r2) := by
   apply SWBisimulation.toWeakBisimulation at h1
   apply SWBisimulation.toWeakBisimulation at h2
-  apply (WeakBisimulation.iff_swBisimulation lts (r1.comp r2)).1
+  apply (WeakBisimulation.iff_swBisimulation lts (Relation.Comp r1 r2)).1
   apply WeakBisimulation.comp lts r1 r2 h1 h2
 
 /-- Weak bisimilarity is transitive. -/
@@ -1114,10 +1113,10 @@ theorem WeakBisimilarity.trans
   s1 ≈[lts] s3 := by
   obtain ⟨r1, hr1, hr1b⟩ := h1
   obtain ⟨r2, hr2, hr2b⟩ := h2
-  exists r1.comp r2
+  exists Relation.Comp r1 r2
   constructor
   case left =>
-    simp only [Rel.comp]
+    simp only [Relation.Comp]
     exists s2
   case right =>
     apply WeakBisimulation.comp lts r1 r2 hr1b hr2b
diff --git a/Cslib/Semantics/LTS/Simulation.lean b/Cslib/Semantics/LTS/Simulation.lean
index 10afc985..3972f2e5 100644
--- a/Cslib/Semantics/LTS/Simulation.lean
+++ b/Cslib/Semantics/LTS/Simulation.lean
@@ -5,7 +5,7 @@ Authors: Fabrizio Montesi
 -/
 
 import Cslib.Semantics.LTS.Basic
-import Cslib.Utils.Rel
+import Cslib.Data.Relation
 
 /-! # Simulation and Similarity
 
@@ -46,13 +46,13 @@ variable {State : Type u} {Label : Type v} (lts : LTS State Label)
 /-- A relation is a simulation if, whenever it relates two states in an lts,
 any transition originating from the first state is mimicked by a transition from the second state
 and the reached derivatives are themselves related. -/
-def Simulation (lts : LTS State Label) (r : Rel State State) : Prop :=
+def Simulation (lts : LTS State Label) (r : State → State → Prop) : Prop :=
   ∀ s1 s2, r s1 s2 → ∀ μ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2'
 
 /-- Two states are similar if they are related by some simulation. -/
-def Similarity (lts : LTS State Label) : Rel State State :=
+def Similarity (lts : LTS State Label) : State → State → Prop :=
   fun s1 s2 =>
-    ∃ r : Rel State State, r s1 s2 ∧ Simulation lts r
+    ∃ r : State → State → Prop, r s1 s2 ∧ Simulation lts r
 
 /--
 Notation for similarity.
@@ -64,7 +64,7 @@ notation s:max " ≤[" lts "] " s':max => Similarity lts s s'
 
 /-- Similarity is reflexive. -/
 theorem Similarity.refl (s : State) : s ≤[lts] s := by
-  exists Rel.Id
+  exists Relation.Id
   apply And.intro (by constructor)
   simp only [Simulation]
   intro s1 s2 hr μ s1' htr
@@ -74,8 +74,8 @@ theorem Similarity.refl (s : State) : s ≤[lts] s := by
 
 /-- The composition of two simulations is a simulation. -/
 theorem Simulation.comp
-  (r1 r2 : Rel State State) (h1 : Simulation lts r1) (h2 : Simulation lts r2) :
-  Simulation lts (r1.comp r2) := by
+  (r1 r2 : State → State → Prop) (h1 : Simulation lts r1) (h2 : Simulation lts r2) :
+  Simulation lts (Relation.Comp r1 r2) := by
   simp_all only [Simulation]
   intro s1 s2 hrc μ s1' htr
   rcases hrc with ⟨sb, hr1, hr2⟩
@@ -88,24 +88,24 @@ theorem Simulation.comp
   exists s2''
   constructor
   · exact h2'tr
-  · simp [Rel.comp]
+  · simp only [Relation.Comp]
     exists s1''
 
 /-- Similarity is transitive. -/
 theorem Similarity.trans (h1 : s1 ≤[lts] s2) (h2 : s2 ≤[lts] s3) : s1 ≤[lts] s3 := by
   obtain ⟨r1, hr1, hr1s⟩ := h1
   obtain ⟨r2, hr2, hr2s⟩ := h2
-  exists r1.comp r2
+  exists Relation.Comp r1 r2
   constructor
   case left =>
-    simp only [Rel.comp]
+    simp only [Relation.Comp]
     exists s2
   case right =>
     apply Simulation.comp lts r1 r2 hr1s hr2s
 
 /-- Simulation equivalence relates all states `s1` and `s2` such that `s1 ≤[lts] s2` and
 `s2 ≤[lts] s1`. -/
-def SimulationEquiv (lts : LTS State Label) : Rel State State :=
+def SimulationEquiv (lts : LTS State Label) : State → State → Prop :=
   fun s1 s2 =>
     s1 ≤[lts] s2 ∧ s2 ≤[lts] s1
 
@@ -117,7 +117,7 @@ notation s:max " ≤≥[" lts "] " s':max => SimulationEquiv lts s s'
 /-- Simulation equivalence is reflexive. -/
 theorem SimulationEquiv.refl (s : State) : s ≤≥[lts] s := by
   simp [SimulationEquiv]
-  exists Rel.Id
+  exists Relation.Id
   constructor; constructor
   simp only [Simulation]
   intro s1 s2 hr μ s1' htr
@@ -142,17 +142,17 @@ theorem SimulationEquiv.trans {s1 s2 s3 : State} (h1 : s1 ≤≥[lts] s2) (h2 :
   case left =>
     obtain ⟨r1, hr1, hr1s⟩ := h1l
     obtain ⟨r2, hr2, hr2s⟩ := h2l
-    exists r1.comp r2
+    exists Relation.Comp r1 r2
     constructor
-    · simp only [Rel.comp]
+    · simp only [Relation.Comp]
       exists s2
     · apply Simulation.comp lts r1 r2 hr1s hr2s
   case right =>
     obtain ⟨r1, hr1, hr1s⟩ := h1r
     obtain ⟨r2, hr2, hr2s⟩ := h2r
-    exists r2.comp r1
+    exists Relation.Comp r2 r1
     constructor
-    · simp only [Rel.comp]
+    · simp only [Relation.Comp]
       exists s2
     · apply Simulation.comp lts r2 r1 hr2s hr1s
 
diff --git a/Cslib/Utils/Rel.lean b/Cslib/Utils/Rel.lean
deleted file mode 100644
index 10ff4751..00000000
--- a/Cslib/Utils/Rel.lean
+++ /dev/null
@@ -1,18 +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
--/
-
-import Mathlib.Data.Rel
-
-/-- Union of two relations. -/
-def Rel.union {α β} (r s : Rel α β) : Rel α β :=
-  fun x y => r x y ∨ s x y
-
-/-- The relation `r` 'up to' the relation `s`. -/
-def Rel.upTo {α} (r s : Rel α α) : Rel α α := s.comp (r.comp s)
-
-/-- The identity relation. -/
-inductive Rel.Id {α} : Rel α α where
-| id {x : α} : Rel.Id x x
diff --git a/Cslib/Utils/Relation.lean b/Cslib/Utils/Relation.lean
deleted file mode 100644
index ceaf7382..00000000
--- a/Cslib/Utils/Relation.lean
+++ /dev/null
@@ -1,77 +0,0 @@
-/-
-Copyright (c) 2025 Thomas Waring. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Thomas Waring, Chris Henson
--/
-import Mathlib.Logic.Relation
-
-universe u
-
-variable {α : Type u} {R R' : α → α → Prop}
-
-/-- A relation has the diamond property when all reductions with a common origin are joinable -/
-abbrev Diamond (R : α → α → Prop) := ∀ {A B C : α}, R A B → R A C → (∃ D, R B D ∧ R C D)
-
-/-- A relation is confluent when its reflexive transitive closure has the diamond property. -/
-abbrev Confluence (R : α → α → Prop) := Diamond (Relation.ReflTransGen R)
-
-/-- Extending a multistep reduction by a single step preserves multi-joinability. -/
-lemma Relation.ReflTransGen.diamond_extend (h : Diamond R) : 
-  Relation.ReflTransGen R A B → 
-  R A C → 
-  ∃ D, Relation.ReflTransGen R B D ∧ Relation.ReflTransGen R C D := by
-  intros AB _
-  revert C
-  induction AB using Relation.ReflTransGen.head_induction_on <;> intros C AC
-  case refl => exact ⟨C, ⟨single AC, by rfl⟩⟩
-  case head A'_C' _ ih =>
-    obtain ⟨D, ⟨CD, C'_D⟩⟩ := h AC A'_C'
-    obtain ⟨D', ⟨B_D', D_D'⟩⟩ := ih C'_D
-    exact ⟨D', ⟨B_D', head CD D_D'⟩⟩
-
-/-- The diamond property implies confluence. -/
-theorem Relation.ReflTransGen.diamond_confluence (h : Diamond R) : Confluence R := by
-  intros A B C AB BC
-  revert C
-  induction AB using Relation.ReflTransGen.head_induction_on <;> intros C BC
-  case refl => exists C
-  case head _ _ A'_C' _ ih =>
-    obtain ⟨D, ⟨CD, C'_D⟩⟩ := diamond_extend h BC A'_C'
-    obtain ⟨D', ⟨B_D', D_D'⟩⟩ := ih C'_D
-    exact ⟨D', ⟨B_D', trans CD D_D'⟩⟩
-
--- not sure why this doesn't compile as an "instance" but oh well
-def trans_of_subrelation {α : Type _} (s s' r : α → α → Prop) (hr : Transitive r)
-    (h : ∀ a b : α, s a b → r a b) (h' : ∀ a b : α, s' a b → r a b) : Trans s s' r where
-  trans := by
-    intro a b c hab hbc
-    replace hab := h _ _ hab
-    replace hbc := h' _ _ hbc
-    exact hr hab hbc
-
-def trans_of_subrelation_left {α : Type _} (s r : α → α → Prop) (hr : Transitive r)
-    (h : ∀ a b : α, s a b → r a b) : Trans s r r where
-  trans := by
-    intro a b c hab hbc
-    replace hab := h _ _ hab
-    exact hr hab hbc
-
-def trans_of_subrelation_right {α : Type _} (s r : α → α → Prop) (hr : Transitive r)
-    (h : ∀ a b : α, s a b → r a b) : Trans r s r where
-  trans := by
-    intro a b c hab hbc
-    replace hbc := h _ _ hbc
-    exact hr hab hbc
-
-/-- This is a straightforward but useful specialisation of a more general result in
-`Mathlib.Logic.Relation`. -/
-theorem church_rosser_of_diamond {α : Type _} {r : α → α → Prop}
-    (h : ∀ a b c, r a b → r a c → Relation.Join r b c) :
-    Equivalence (Relation.Join (Relation.ReflTransGen r)) := by
-  apply Relation.equivalence_join_reflTransGen
-  intro a b c hab hac
-  let ⟨d, hd⟩ := h a b c hab hac
-  use d
-  constructor
-  . exact Relation.ReflGen.single hd.1
-  . exact Relation.ReflTransGen.single hd.2
diff --git a/CslibTests/Bisimulation.lean b/CslibTests/Bisimulation.lean
index 2b30fbbb..ca68989c 100644
--- a/CslibTests/Bisimulation.lean
+++ b/CslibTests/Bisimulation.lean
@@ -19,7 +19,7 @@ private inductive tr1 : ℕ → Char → ℕ → Prop where
 
 def lts1 := LTS.mk tr1
 
-private inductive Bisim15 : Rel ℕ ℕ where
+private inductive Bisim15 : ℕ → ℕ → Prop where
 | oneFive : Bisim15 1 5
 | twoSix : Bisim15 2 6
 | threeSeven : Bisim15 3 7
diff --git a/CslibTests/LTS.lean b/CslibTests/LTS.lean
index 4fc4021d..78904276 100644
--- a/CslibTests/LTS.lean
+++ b/CslibTests/LTS.lean
@@ -23,7 +23,7 @@ theorem NatTr.dom : NatTr n μ m → (n = 1 ∨ n = 2) ∧ (m = 1 ∨ m = 2) :=
 
 def natLts : LTS ℕ ℕ := ⟨NatTr⟩
 
-inductive NatBisim : Rel ℕ ℕ where
+inductive NatBisim : ℕ → ℕ → Prop where
 | one_one : NatBisim 1 1
 | one_two : NatBisim 1 2
 | two_one : NatBisim 2 1