diff --git a/Cslib/Foundations/Logic/InferenceSystem.lean b/Cslib/Foundations/Logic/InferenceSystem.lean
index 854b8deb1..3067d3f6c 100644
--- a/Cslib/Foundations/Logic/InferenceSystem.lean
+++ b/Cslib/Foundations/Logic/InferenceSystem.lean
@@ -8,7 +8,15 @@ module
 
 public import Cslib.Init
 
-/-! -/
+/-! # Inference systems
+
+This module defines the basic classes and notation for *inference systems* -- systems for deriving
+conclusions from premises.
+
+We intend inference systems broadly, as in theory of programming languages. In applications to
+logic, for example, we use inference systems to capture both the concepts of satisfiability and
+proof systems.
+-/
 
 @[expose] public section
 
@@ -63,6 +71,17 @@ noncomputable instance [InferenceSystem S α] {a : α} : Coe (DerivableIn S a) (
 
 @[inherit_doc] scoped notation "⇓" a:90 => InferenceSystem.derivation Default a
 
+open Lean Elab PrettyPrinter Delaborator SubExpr in
+/-- Delaborator that hides `InferenceSystem.Default` in uses of the `⇓a` notation. -/
+@[app_delab InferenceSystem.derivation]
+meta def delabInferenceSystem : Delab := do
+  let expr ← getExpr
+  if expr.getAppArgs[0]?.any (·.isConstOf `Cslib.Logic.InferenceSystem.Default) then
+    let a ← withAppArg delab
+    `(⇓ $a)
+  else
+    delabApp
+
 end InferenceSystem
 
 end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/LogicalEquivalence.lean b/Cslib/Foundations/Logic/LogicalEquivalence.lean
index f4dbc06d9..9885b5066 100644
--- a/Cslib/Foundations/Logic/LogicalEquivalence.lean
+++ b/Cslib/Foundations/Logic/LogicalEquivalence.lean
@@ -18,31 +18,13 @@ namespace Cslib.Logic
 
 open scoped InferenceSystem
 
-/-- A logical equivalence for a given type of `Judgement`s is a congruence on propositions that
-preserves validity of judgements under any judgemental context. -/
-class LogicalEquivalence S
-    (Proposition : Type u) [HasContext Proposition]
-    (Judgement : Type v) [HasHContext Judgement Proposition]
-    [InferenceSystem S Judgement] where
-  /-- `a ≡[S] b` means that `a` and `b` are logically equivalent in the inference system `S`. -/
-  eqv (a b : Proposition) : Prop
-  /-- Proof that `eqv` is a congruence. -/
-  [congruence : Congruence Proposition eqv]
+/-- A logical equivalence `eqv` for an inference system `S` is a congruence on propositions (of type
+`α`) that preserves validity of judgements under any judgemental context. -/
+class LogicalEquivalence S (eqv : α → α → Prop)
+    [HasContext α] [Congruence eqv] [HasHContext Judgement α] [InferenceSystem S Judgement]
+    extends LawfulCongruence eqv where
   /-- Validity is preserved for any judgemental context. -/
-  eqvFillValid (heqv : eqv a b) (c : HasHContext.Context Judgement Proposition)
+  eqvFillValid (heqv : a ≡[eqv] b) (c : HasHContext.Context Judgement α)
     (h : S⇓(c<[a])) : S⇓(c<[b])
 
-@[inherit_doc]
-scoped notation a " ≡[" S "]" b => LogicalEquivalence.eqv S a b
-
-/-- Class for types (`α`) that have a canonical logical equivalence (under a canonical, default
-inference system). -/
-abbrev HasLogicalEquivalence (Proposition : Type u) [HasContext Proposition]
-    (Judgement : Type v) [HasHContext Judgement Proposition]
-    [HasInferenceSystem Judgement] :=
-  LogicalEquivalence InferenceSystem.Default Proposition Judgement
-
-/-- `a ≡ b` means that `a` and `b` are logically equivalent. -/
-scoped infix:29 " ≡ " => LogicalEquivalence.eqv InferenceSystem.Default
-
 end Cslib.Logic
diff --git a/Cslib/Foundations/Syntax/Congruence.lean b/Cslib/Foundations/Syntax/Congruence.lean
index 0a787a642..25c954c2d 100644
--- a/Cslib/Foundations/Syntax/Congruence.lean
+++ b/Cslib/Foundations/Syntax/Congruence.lean
@@ -15,8 +15,36 @@ public import Mathlib.Algebra.Order.Monoid.Unbundled.Defs
 
 namespace Cslib
 
-/-- An equivalence relation on `α` preserved by all contexts `Ctx`. -/
-class Congruence (α : Type*) [HasContext α] (r : α → α → Prop) extends
-  IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) r
+/-- The relation `r` is a congruence on `α`. This class gives access to the `≡[r]` notation.
+To instantiate a canonical congruence for `α`, see `HasCongruence`.
+
+Congruence relations should also instantiate `LawfulCongruence` to prove that the relation respects
+the expected congruence laws. -/
+class Congruence (r : α → α → Prop)
+
+/-- `a ≡[r] b` means that the `a` and `b` are related by the congruence `r`. -/
+@[nolint unusedArguments]
+def Congruence.r (r : α → α → Prop) [Congruence r] := r
+
+@[inherit_doc]
+scoped notation:29 a " ≡[" r "] " b => Congruence.r r a b
+
+/-- The type `α` has a canonical congruence relation. This gives access to the `≡` notation. -/
+class DefaultCongruence (α : Type*) (r : outParam (α → α → Prop))
+
+/-- `a ≡ b` means that `a` and `b` are related by the canonical congruence relation for their
+type. -/
+@[nolint unusedArguments]
+def DefaultCongruence.r {α : Type*} {r : α → α → Prop} [DefaultCongruence α r] (a b : α) := r a b
+
+@[inherit_doc]
+scoped infix:29 " ≡ " => DefaultCongruence.r
+
+@[nolint unusedArguments]
+instance (α : Type*) (r : α → α → Prop) [DefaultCongruence α r] : Congruence r := ⟨⟩
+
+/-- An equivalence relation on `α` preserved by all contexts. -/
+class LawfulCongruence (r : α → α → Prop) [Congruence r] [HasContext α] extends
+  IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) (· ≡[r] ·)
 
 end Cslib
diff --git a/Cslib/Foundations/Syntax/Context.lean b/Cslib/Foundations/Syntax/Context.lean
index 6f9c7c83c..196702992 100644
--- a/Cslib/Foundations/Syntax/Context.lean
+++ b/Cslib/Foundations/Syntax/Context.lean
@@ -17,7 +17,7 @@ namespace Cslib
 /-- Class for types with a canonical notion of heterogeneous single-hole contexts. -/
 class HasHContext (α β : Type*) where
   /-- The type of contexts. -/
-  Context : Type*
+  {Context : Type*}
   /-- Replaces the hole in the context with a value, resulting in a new value. -/
   fill (c : Context) (b : β) : α
 
diff --git a/Cslib/Languages/CCS/Basic.lean b/Cslib/Languages/CCS/Basic.lean
index c30c1849d..ec581611c 100644
--- a/Cslib/Languages/CCS/Basic.lean
+++ b/Cslib/Languages/CCS/Basic.lean
@@ -119,7 +119,7 @@ def Context.fill (c : Context Name Constant) (p : Process Name Constant) : Proce
   | choiceR r c => Process.choice r (c.fill p)
   | res a c => Process.res a (c.fill p)
 
-instance : HasContext (Process Name Constant) := ⟨Context Name Constant, Context.fill⟩
+instance : HasContext (Process Name Constant) := ⟨Context.fill⟩
 
 /-- Definition of context filling. -/
 @[scoped grind =]
diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index d71ece490..cd5a00f9d 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -441,10 +441,14 @@ theorem bisimilarity_is_congruence
   | _ => grind [bisimilarity_congr_pre, bisimilarity_congr_par,
                 bisimilarity_congr_choice, bisimilarity_congr_res]
 
+instance : Congruence (HomBisimilarity (lts (defs := defs))) := ⟨⟩
+
 /-- Bisimilarity is a congruence in CCS. -/
 instance bisimilarityCongruence :
-    Congruence (Process Name Constant) (HomBisimilarity (lts (defs := defs))) where
-  covariant := ⟨by grind [Covariant, bisimilarity_is_congruence]⟩
+    LawfulCongruence (HomBisimilarity (lts (defs := defs))) where
+  elim := by
+    dsimp [Congruence.r]
+    grind [Covariant, bisimilarity_is_congruence]
 
 end CCS
 
diff --git a/Cslib/Logics/HML/Basic.lean b/Cslib/Logics/HML/Basic.lean
index de2efd0ca..1bba83dd3 100644
--- a/Cslib/Logics/HML/Basic.lean
+++ b/Cslib/Logics/HML/Basic.lean
@@ -7,6 +7,8 @@ Authors: Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker
 module
 
 public import Cslib.Foundations.Semantics.LTS.Bisimulation
+public import Cslib.Foundations.Logic.Operators
+public import Cslib.Foundations.Logic.InferenceSystem
 
 /-! # Hennessy-Milner Logic (HML)
 
@@ -16,9 +18,8 @@ concurrent systems.
 ## Implementation notes
 There are two main versions of HML. The original [Hennessy1985], which includes a negation
 connective, and a variation without negation, for example as in [Aceto1999].
-We follow the latter, which is used in many recent papers. Negation is recovered as usual, by having
-a `false` atomic proposition and a function that, given any proposition, returns its negated form
-(see `Proposition.neg`).
+We follow the former and focus on a minimal set of connectives, recovering the others as derived
+constructs.
 
 ## Main definitions
 
@@ -50,67 +51,197 @@ namespace Cslib.Logic.HML
 
 /-- Propositions. -/
 inductive Proposition (Label : Type u) : Type u where
+  /-- Truth. -/
   | true
-  | false
+  /-- Conjunction. -/
   | and (φ₁ φ₂ : Proposition Label)
-  | or (φ₁ φ₂ : Proposition Label)
+  /-- Negation. -/
+  | not (φ : Proposition Label)
+  /-- Possibility (dynamic diamond modality). -/
   | diamond (μ : Label) (φ : Proposition Label)
-  | box (μ : Label) (φ : Proposition Label)
 
-/-- Negation of a proposition. -/
-@[simp, scoped grind =]
-def Proposition.neg (a : Proposition Label) : Proposition Label :=
-  match a with
-  | .true => .false
-  | .false => .true
-  | and a b => or a.neg b.neg
-  | or a b => and a.neg b.neg
-  | diamond μ a => box μ a.neg
-  | box μ a => diamond μ a.neg
+instance : Top (Proposition Label) := ⟨.true⟩
+instance : HasAnd (Proposition Label) := ⟨.and⟩
+instance : HasNot (Proposition Label) := ⟨.not⟩
+instance : HasDynamicDiamond (Proposition Label) Label := ⟨.diamond⟩
+
+/-- Falsity, derived from negation and truth. -/
+@[match_pattern]
+def Proposition.false : Proposition Label := ¬⊤
+
+instance : Bot (Proposition Label) := ⟨.false⟩
+
+/-- Disjunction, derived from negation and conjunction. -/
+@[match_pattern]
+def Proposition.or (φ₁ φ₂ : Proposition Label) : Proposition Label := ¬(¬φ₁ ∧ ¬φ₂)
+
+instance : HasOr (Proposition Label) := ⟨Proposition.or⟩
+
+/-- Implication. -/
+@[match_pattern]
+def Proposition.imp (φ₁ φ₂ : Proposition Label) : Proposition Label := ¬φ₁ ∨ φ₂
+
+instance : HasImp (Proposition Label) := ⟨.imp⟩
+
+/-- Bi-implication. -/
+@[match_pattern]
+def Proposition.iff (φ₁ φ₂ : Proposition Label) : Proposition Label := (φ₁ → φ₂) ∧ (φ₂ → φ₁)
+
+instance : HasIff (Proposition Label) := ⟨.iff⟩
+
+/-- Necessity (dynamic box modality), derived from dynamic diamond and negation. -/
+@[match_pattern]
+def Proposition.box (μ : Label) (φ : Proposition Label) : Proposition Label := ¬d⟨μ⟩¬φ
+
+instance : HasDynamicBox (Proposition Label) Label := ⟨.box⟩
+
+@[scoped grind =]
+lemma Proposition.top_def : .true = ((⊤ : Proposition Label)) := rfl
+
+@[scoped grind =]
+lemma Proposition.bot_def : .false = ((⊥ : Proposition Label)) := rfl
+
+@[scoped grind =]
+lemma Proposition.and_def (φ₁ φ₂ : Proposition Label) : φ₁.and φ₂ = (φ₁ ∧ φ₂) := rfl
+
+@[scoped grind =]
+lemma Proposition.not_def (φ : Proposition Label) : φ.not = ¬φ := rfl
+
+@[scoped grind =]
+lemma Proposition.diamond_def (μ : Label) (φ : Proposition Label) :
+  Proposition.diamond μ φ = d⟨μ⟩φ := rfl
+
+@[scoped grind =]
+lemma Proposition.or_def (φ₁ φ₂ : Proposition Label) : φ₁.or φ₂ = (φ₁ ∨ φ₂) := rfl
+
+@[scoped grind =]
+lemma Proposition.imp_def (φ₁ φ₂ : Proposition Label) : φ₁.imp φ₂ = (φ₁ → φ₂) := rfl
+
+@[scoped grind =]
+lemma Proposition.iff_def (φ₁ φ₂ : Proposition Label) :
+    φ₁.iff φ₂ = (φ₁ ↔ φ₂) := rfl
+
+@[scoped grind =]
+lemma Proposition.box_def (μ : Label) (φ : Proposition Label) : Proposition.box μ φ = d[μ]φ := rfl
 
 /-- Finite conjunction of propositions. -/
 @[simp, scoped grind =]
-def Proposition.finiteAnd (as : List (Proposition Label)) : Proposition Label :=
-  List.foldr .and .true as
+def Proposition.finiteAnd (φs : List (Proposition Label)) : Proposition Label :=
+  List.foldr (· ∧ ·) ⊤ φs
 
 /-- Finite disjunction of propositions. -/
 @[simp, scoped grind =]
-def Proposition.finiteOr (as : List (Proposition Label)) : Proposition Label :=
-  List.foldr .or .false as
+def Proposition.finiteOr (φs : List (Proposition Label)) : Proposition Label :=
+  List.foldr (· ∨ ·) ⊥ φs
 
-/-- Satisfaction relation. `Satisfies lts s a` means that, in the LTS `lts`, the state `s` satisfies
-the proposition `a`. -/
+/-- Satisfaction relation. `Satisfies lts s φ` means that, in the LTS `lts`, the state `s` satisfies
+the proposition `φ`. -/
 @[scoped grind]
-inductive Satisfies (lts : LTS State Label) : State → Proposition Label → Prop where
-  | true {s : State} : Satisfies lts s .true
-  | and {s : State} {a b : Proposition Label} :
-    Satisfies lts s a → Satisfies lts s b →
-    Satisfies lts s (.and a b)
-  | or₁ {s : State} {a b : Proposition Label} :
-    Satisfies lts s a → Satisfies lts s (.or a b)
-  | or₂ {s : State} {a b : Proposition Label} :
-    Satisfies lts s b → Satisfies lts s (.or a b)
-  | diamond {s s' : State} {μ : Label} {a : Proposition Label}
-    (htr : lts.Tr s μ s') (hs : Satisfies lts s' a) : Satisfies lts s (.diamond μ a)
-  | box {s : State} {μ : Label} {a : Proposition Label}
-    (h : ∀ s', lts.Tr s μ s' → Satisfies lts s' a) :
-    Satisfies lts s (.box μ a)
+def Satisfies (lts : LTS State Label) (s : State) : Proposition Label → Prop
+  | .true => True
+  | .and φ₁ φ₂ => Satisfies lts s φ₁ ∧ Satisfies lts s φ₂
+  | .not φ => ¬Satisfies lts s φ
+  | .diamond μ φ => ∃ s', lts.Tr s μ s' ∧ Satisfies lts s' φ
+
+/-- Judgement, representing the conclusions one reaches in HML. -/
+structure Judgement State Label where
+  /-- Constructs a judgement. -/
+  mk ::
+  /-- LTS. -/
+  lts : LTS State Label
+  /-- The state satisfying the proposition `φ`. -/
+  state : State
+  /-- The proposition satisfied by the state `s`. -/
+  φ : Proposition Label
+
+@[inherit_doc] scoped notation "HML[" lts "," s " ⊨ " φ "]" => Judgement.mk lts s φ
+
+/-- Satisfaction for judgements. This just refers to the unbundled `Satisfies`. -/
+@[simp, scoped grind =]
+def Satisfies.Bundled (j : Judgement State Label) : Prop := Satisfies j.lts j.state j.φ
+
+instance : HasInferenceSystem (Judgement State Label) := ⟨Satisfies.Bundled⟩
+
+open scoped InferenceSystem Proposition
+
+@[scoped grind =]
+theorem derivation_def : Satisfies lts s φ = ⇓HML[lts,s ⊨ φ] := rfl
+
+@[scoped grind =]
+theorem Satisfies.not_iff_not : ⇓HML[lts,s ⊨ ¬φ] ↔ ¬⇓HML[lts,s ⊨ φ] := by rfl
+
+@[scoped grind .]
+theorem Satisfies.top : ⇓HML[lts,s ⊨ ⊤] := by
+  dsimp [Top.top]
+  grind [=_ derivation_def]
+
+@[scoped grind .]
+theorem Satisfies.bot : ¬⇓HML[lts,s ⊨ ⊥] := by
+  simp only [Bot.bot]
+  grind [= Proposition.false]
+
+@[scoped grind =]
+theorem Satisfies.and_iff_and :
+    ⇓HML[lts,s ⊨ φ₁ ∧ φ₂] ↔ ⇓HML[lts,s ⊨ φ₁] ∧ ⇓HML[lts,s ⊨ φ₂] := by rfl
+
+@[scoped grind =]
+theorem Satisfies.or_iff_or :
+    ⇓HML[lts,s ⊨ φ₁ ∨ φ₂] ↔ ⇓HML[lts,s ⊨ φ₁] ∨ ⇓HML[lts,s ⊨ φ₂] := by
+  grind [=_ Proposition.or_def, Proposition.or]
+
+@[scoped grind =]
+theorem Satisfies.diamond_iff_exists :
+    ⇓HML[lts,s ⊨ d⟨μ⟩φ] ↔ ∃ s', lts.Tr s μ s' ∧ ⇓HML[lts,s' ⊨ φ] := by rfl
+
+/-- Characterisation of the `→` connective.
+
+Implication is defined in terms of the more primitive connectives given in `Proposition`.
+This result proves that the definition is correct.
+-/
+@[scoped grind =]
+theorem Satisfies.imp_iff_imp :
+    ⇓HML[lts,s ⊨ φ₁ → φ₂] ↔ (⇓HML[lts,s ⊨ φ₁] → ⇓HML[lts,s ⊨ φ₂]) := by
+  grind [=_ Proposition.imp_def, Proposition.imp]
+
+/-- Characterisation of the `↔` connective.
+
+Bi-implication is defined in terms of the more primitive connectives given in `Proposition`.
+This result proves that the definition is correct. -/
+@[scoped grind =]
+theorem Satisfies.iff_iff_iff :
+    ⇓HML[lts,s ⊨ φ₁ ↔ φ₂] ↔ (⇓HML[lts,s ⊨ φ₁] ↔ ⇓HML[lts,s ⊨ φ₂]) := by
+  simp only [HasIff.iff, Proposition.iff]
+  grind
+
+@[scoped grind =]
+theorem Satisfies.box_iff_forall :
+    ⇓HML[lts,s ⊨ d[μ]φ] ↔ ∀ s', lts.Tr s μ s' → ⇓HML[lts,s' ⊨ φ] := by
+  grind [=_ Proposition.box_def, Proposition.box]
+
+/-- A state satisfies a finite conjunction iff it satisfies all conjuncts. -/
+@[scoped grind =]
+theorem Satisfies.finiteAnd_iff_forall :
+    ⇓HML[lts,s ⊨ Proposition.finiteAnd φs] ↔ ∀ φ ∈ φs, ⇓HML[lts,s ⊨ φ] := by
+  induction φs <;> grind
+
+/-- A state satisfies a finite disjunction iff it satisfies some disjunct. -/
+@[scoped grind =]
+theorem Satisfies.finiteOr_iff_exists :
+    ⇓HML[lts,s ⊨ Proposition.finiteOr φs] ↔ ∃ φ ∈ φs, ⇓HML[lts,s ⊨ φ] := by
+  induction φs <;> grind
 
 /-- Denotation of a proposition. -/
 @[simp, scoped grind =]
-def Proposition.denotation (a : Proposition Label) (lts : LTS State Label)
-    : Set State :=
-  match a with
+def Proposition.denotation (lts : LTS State Label)
+    : Proposition Label → Set State
   | .true => Set.univ
-  | .false => ∅
-  | .and a b => a.denotation lts ∩ b.denotation lts
-  | .or a b => a.denotation lts ∪ b.denotation lts
-  | .diamond μ a => {s | ∃ s', lts.Tr s μ s' ∧ s' ∈ a.denotation lts}
-  | .box μ a => {s | ∀ s', lts.Tr s μ s' → s' ∈ a.denotation lts}
+  | .and φ₁ φ₂ => φ₁.denotation lts ∩ φ₂.denotation lts
+  | .not φ => (φ.denotation lts)ᶜ
+  | .diamond μ φ => {s | ∃ s', lts.Tr s μ s' ∧ s' ∈ φ.denotation lts}
 
 /-- The theory of a state is the set of all propositions that it satisfies. -/
 abbrev theory (lts : LTS State Label) (s : State) : Set (Proposition Label) :=
-  {a | Satisfies lts s a}
+  {φ | ⇓HML[lts,s ⊨ φ]}
 
 /-- Two states are theory-equivalent (for a specific LTS) if they have the same theory. -/
 abbrev TheoryEq (lts : LTS State Label) (s1 s2 : State) :=
@@ -120,59 +251,46 @@ open Proposition LTS
 
 /-- Characterisation theorem for the denotational semantics. -/
 @[scoped grind =]
-theorem satisfies_mem_denotation {lts : LTS State Label} :
-    Satisfies lts s a ↔ s ∈ a.denotation lts := by
-  induction a generalizing s <;> grind
+theorem mem_denotation_iff_satisfies {φ : Proposition Label} :
+    s ∈ φ.denotation lts ↔ ⇓HML[lts,s ⊨ φ] := by
+  induction φ generalizing s <;> grind [=_ derivation_def]
 
-/-- A state satisfies a proposition iff it does not satisfy the negation of the proposition. -/
-@[simp, scoped grind =]
-theorem neg_satisfies {lts : LTS State Label} :
-    ¬Satisfies lts s a.neg ↔ Satisfies lts s a := by
-  induction a generalizing s <;> grind
+@[scoped grind .]
+theorem mem_theory_iff_satisfies : φ ∈ theory lts s ↔ ⇓HML[lts,s ⊨ φ] := by
+  grind
 
-/-- A state is in the denotation of a proposition iff it is not in the denotation of the negation
-of the proposition. -/
-@[scoped grind =]
-theorem neg_denotation {lts : LTS State Label} (a : Proposition Label) :
-    s ∉ a.neg.denotation lts ↔ s ∈ a.denotation lts := by
-  grind [_=_ satisfies_mem_denotation]
+/- A state satisfies a proposition iff it does not satisfy the negation of the proposition. -/
+-- @[simp, scoped grind =]
+-- theorem Satisfies.not_not_iff {lts : LTS State Label} :
+--   ¬⇓HML[lts,s ⊨ ¬φ] ↔ ⇓HML[lts,s ⊨ φ] := by
+--   grind
 
-/-- A state satisfies a finite conjunction iff it satisfies all conjuncts. -/
-@[scoped grind =]
-theorem satisfies_finiteAnd {lts : LTS State Label} {s : State}
-    {as : List (Proposition Label)} :
-    Satisfies lts s (Proposition.finiteAnd as) ↔ ∀ a ∈ as, Satisfies lts s a := by
-  induction as <;> grind
+open scoped Satisfies
 
-/-- A state satisfies a finite disjunction iff it satisfies some disjunct. -/
+/-- A state is in the denotation of a proposition iff it is not in the denotation of the negation
+of the proposition. -/
 @[scoped grind =]
-theorem satisfies_finiteOr {lts : LTS State Label} {s : State}
-    {as : List (Proposition Label)} :
-    Satisfies lts s (Proposition.finiteOr as) ↔ ∃ a ∈ as, Satisfies lts s a := by
-  induction as <;> grind
-
-@[scoped grind →]
-theorem satisfies_theory (h : Satisfies lts s a) : a ∈ theory lts s := by
-  grind
+theorem not_denotation {lts : LTS State Label} (φ : Proposition Label) :
+    s ∉ (¬φ).denotation lts ↔ s ∈ φ.denotation lts := by grind
 
 /-- Two states are theory-equivalent iff they are denotationally equivalent. -/
 theorem theoryEq_denotation_eq {lts : LTS State Label} :
     TheoryEq lts s1 s2 ↔
-    (∀ a : Proposition Label, s1 ∈ a.denotation lts ↔ s2 ∈ a.denotation lts) := by
-  grind [_=_ satisfies_mem_denotation]
+    (∀ φ : Proposition Label, s1 ∈ φ.denotation lts ↔ s2 ∈ φ.denotation lts) := by
+  grind [=_ mem_theory_iff_satisfies, =_ mem_denotation_iff_satisfies]
 
 /-- If two states are not theory equivalent, there exists a distinguishing proposition. -/
-lemma not_theoryEq_satisfies (h : ¬ TheoryEq lts s1 s2) :
-    ∃ a, (Satisfies lts s1 a ∧ ¬Satisfies lts s2 a) := by
-  grind [=_ neg_satisfies]
+lemma not_theoryEq_satisfies (h : ¬TheoryEq lts s1 s2) :
+    ∃ φ, (⇓HML[lts,s1 ⊨ φ] ∧ ¬⇓HML[lts,s2 ⊨ φ]) := by
+  grind [=_ Satisfies.not_iff_not]
 
 /-- If two states are theory equivalent and the former satisfies a proposition, the latter does as
 well. -/
-theorem theoryEq_satisfies {lts : LTS State Label} (h : TheoryEq lts s1 s2)
-    (hs : Satisfies lts s1 a) : Satisfies lts s2 a := by
+theorem theoryEq_satisfies (h : TheoryEq lts s1 s2)
+    (hs : ⇓HML[lts,s1 ⊨ φ]) : ⇓HML[lts,s2 ⊨ φ] := by
   unfold TheoryEq theory at h
   rw [Set.ext_iff] at h
-  exact (h a).mp hs
+  exact (h φ).mp hs
 
 section ImageToPropositions
 
@@ -188,12 +306,13 @@ theorem propositions_complete (s' : lts.image s μ) : stateMap s' ∈ propositio
   use s', Finset.mem_toList.mpr (Fintype.complete s')
 
 theorem propositions_satisfies_conjunction (htr : lts.Tr s1 μ s1')
-    (hdist_spec : ∀ s2', Satisfies lts s1' (stateMap s2')) :
-    Satisfies lts s1 (.diamond μ <| Proposition.finiteAnd (propositions stateMap)) := by
-  apply Satisfies.diamond htr
-  rw [satisfies_finiteAnd]
-  intro a ha_mem
-  grind [List.mem_map.mp ha_mem]
+    (hdist_spec : ∀ s2', ⇓HML[lts,s1' ⊨ (stateMap s2')]) :
+    ⇓HML[lts,s1 ⊨ d⟨μ⟩finiteAnd (propositions stateMap)] := by
+  rw [Satisfies.diamond_iff_exists]
+  use s1', htr
+  rw [Satisfies.finiteAnd_iff_forall]
+  intro φ hφ_mem
+  grind [List.mem_map.mp hφ_mem]
 
 end ImageToPropositions
 
@@ -208,15 +327,15 @@ theorem theoryEq_isBisimulation (lts : LTS State Label)
   case left =>
     intro s1' htr
     by_contra
-    have hdist : ∀ s2' : lts.image s2 μ, ∃ a, Satisfies lts s1' a ∧ ¬Satisfies lts s2'.val a := by
+    have hdist : ∀ s2' : lts.image s2 μ, ∃ φ, ⇓HML[lts,s1' ⊨ φ] ∧ ¬⇓HML[lts,s2'.val ⊨ φ] := by
       intro ⟨s2', hs2'⟩
       apply not_theoryEq_satisfies
       grind
     choose dist_formula hdist_spec using hdist
     let conjunction := Proposition.finiteAnd (propositions dist_formula)
-    have hs1_diamond : Satisfies lts s1 (.diamond μ conjunction) := by
+    have hs1_diamond : ⇓HML[lts,s1 ⊨ d⟨μ⟩conjunction] := by
       grind [propositions_satisfies_conjunction]
-    cases (theoryEq_satisfies h hs1_diamond) with | @diamond _ s2'' _ _ htr2 hsat =>
+    obtain ⟨s2'', htr2, hsat⟩ := Satisfies.diamond_iff_exists.mp (theoryEq_satisfies h hs1_diamond)
     grind [propositions_complete dist_formula ⟨s2'', htr2⟩]
   case right =>
     -- Symmetric to left case
@@ -228,39 +347,29 @@ theorem theoryEq_isBisimulation (lts : LTS State Label)
       grind
     choose dist_formula hdist_spec using hdist
     let conjunction := Proposition.finiteAnd (propositions dist_formula)
-    have hs2_diamond : Satisfies lts s2 (.diamond μ conjunction) := by
+    have hs2_diamond : ⇓HML[lts,s2 ⊨ d⟨μ⟩conjunction] := by
       grind [propositions_satisfies_conjunction]
-    cases (theoryEq_satisfies h.symm hs2_diamond) with | @diamond _ s1'' _ _ htr1 hsat =>
+    obtain ⟨s1'', htr1, hsat⟩ :=
+      Satisfies.diamond_iff_exists.mp (theoryEq_satisfies h.symm hs2_diamond)
     grind [propositions_complete dist_formula ⟨s1'', htr1⟩]
 
-/-- If two states are in a bisimulation and the former satisfies a proposition, the latter does as
-well. -/
+/-- If two states are in a bisimulation, one satisfies a proposition iff the other does. -/
 @[scoped grind ⇒]
-lemma bisimulation_satisfies {lts : LTS State Label}
-    {hrb : lts.IsHomBisimulation r}
-    (hr : r s1 s2) (a : Proposition Label) (hs : Satisfies lts s1 a) :
-    Satisfies lts s2 a := by
-  induction a generalizing s1 s2 with
-  | diamond => cases hs with | diamond htr _ => grind [hrb.follow_fst hr htr]
-  | _ => grind [IsBisimulation]
-
-lemma bisimulation_TheoryEq {lts : LTS State Label}
-    {hrb : lts.IsHomBisimulation r}
-    (hr : r s1 s2) :
-    TheoryEq lts s1 s2 := by
-  have : s2 ~[lts] s1 := by grind [Bisimilarity.symm]
-  grind
+lemma bisimulation_satisfies {hrb : lts.IsHomBisimulation r}
+    (hr : r s1 s2) (φ : Proposition Label) : ⇓HML[lts,s1 ⊨ φ] ↔ ⇓HML[lts,s2 ⊨ φ] := by
+  induction φ generalizing s1 s2 <;> grind [IsBisimulation]
+
+lemma bisimulation_theoryEq {hrb : lts.IsHomBisimulation r} (hr : r s1 s2) :
+    TheoryEq lts s1 s2 := by grind
 
 /-- Theory equivalence and bisimilarity coincide for image-finite LTSs. -/
-theorem theoryEq_eq_bisimilarity (lts : LTS State Label)
+theorem theoryEq_eq_bisimilarity {lts : LTS State Label}
     [image_finite : ∀ s μ, Finite (lts.image s μ)] :
     TheoryEq lts = HomBisimilarity lts := by
   ext s1 s2
   apply Iff.intro <;> intro h
   · exists TheoryEq lts
     grind
-  · obtain ⟨r, hr, hrb⟩ := h
-    apply bisimulation_TheoryEq hr
-    exact hrb
+  · grind
 
 end Cslib.Logic.HML
diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean
index 2e0c8005a..5debc60b4 100644
--- a/Cslib/Logics/HML/LogicalEquivalence.lean
+++ b/Cslib/Logics/HML/LogicalEquivalence.lean
@@ -18,24 +18,49 @@ This module defines logical equivalence for HML propositions and instantiates `L
 
 namespace Cslib.Logic.HML
 
-/-- Logical equivalence for HML propositions. -/
-def Proposition.Equiv {State : Type u} {Label : Type v} (a b : Proposition Label) : Prop :=
-  ∀ lts : LTS State Label, a.denotation lts = b.denotation lts
+open scoped InferenceSystem Satisfies
+
+section Theory
+
+/-! ## Theory of logical equivalence -/
+
+/-- The HML propositions `φ₁` and `φ₂` are logically equivalent under the LTS `lts`. -/
+def Proposition.Equiv (lts : LTS State Label) (φ₁ φ₂ : Proposition Label) : Prop :=
+  ∀ (s : State), ⇓HML[lts,s ⊨ φ₁ ↔ φ₂]
+
+instance : Congruence (Proposition.Equiv lts) := ⟨⟩
 
 @[scoped grind =]
-theorem Proposition.equiv_def {State : Type u} {Label : Type v} (a b : Proposition Label) :
-    Equiv (State := State) a b ↔
-    (∀ lts : LTS State Label, a.denotation lts = b.denotation lts) := by rfl
+theorem Proposition.equiv_def (lts : LTS State Label) (φ₁ φ₂ : Proposition Label) :
+    (φ₁.Equiv lts φ₂) ↔ φ₁ ≡[Equiv lts] φ₂ := by rfl
+
+@[scoped grind ⇒]
+theorem Proposition.equiv_forall_der (lts : LTS State Label) (φ₁ φ₂ : Proposition Label)
+    (h : φ₁ ≡[Equiv lts] φ₂) : ∀ (s : State), ⇓HML[lts,s ⊨ φ₁ ↔ φ₂] := by
+  intro s
+  specialize h s
+  assumption
+
+theorem Proposition.forall_der_equiv (lts : LTS State Label) (φ₁ φ₂ : Proposition Label)
+    (h : ∀ (s : State), ⇓HML[lts,s ⊨ φ₁ ↔ φ₂]) :
+    φ₁ ≡[Equiv lts] φ₂ := by
+  intro s
+  specialize h s
+  assumption
+
+@[scoped grind ⇒]
+theorem Proposition.equiv_iff {lts : LTS State Label} {φ₁ φ₂ : Proposition Label}
+    (h : φ₁ ≡[Equiv lts] φ₂) (s : State) :
+    ⇓HML[lts,s ⊨ φ₁] ↔ ⇓HML[lts,s ⊨ φ₂] := by
+  grind [=_ Satisfies.iff_iff_iff]
 
 /-- Propositional contexts. -/
 inductive Proposition.Context (Label : Type u) : Type u where
   | hole
   | andL (c : Context Label) (φ : Proposition Label)
   | andR (φ : Proposition Label) (c : Context Label)
-  | orL (c : Context Label) (φ : Proposition Label)
-  | orR (φ : Proposition Label) (c : Context Label)
+  | not (c : Context Label)
   | diamond (μ : Label) (c : Context Label)
-  | box (μ : Label) (c : Context Label)
 
 /-- Replaces a hole in a propositional context with a proposition. -/
 @[scoped grind =]
@@ -44,74 +69,125 @@ def Proposition.Context.fill (c : Context Label) (φ : Proposition Label) :=
   | hole => φ
   | andL c φ' => (c.fill φ).and φ'
   | andR φ' c => φ'.and (c.fill φ)
-  | orL c φ' => (c.fill φ).or φ'
-  | orR φ' c => φ'.or (c.fill φ)
+  | not c => .not (c.fill φ)
   | diamond μ c => .diamond μ (c.fill φ)
-  | box μ c => .box μ (c.fill φ)
 
-instance : HasContext (Proposition Label) := ⟨Proposition.Context Label, Proposition.Context.fill⟩
+instance : HasContext (Proposition Label) := ⟨Proposition.Context.fill⟩
+
+@[scoped grind =]
+lemma Proposition.Context.fill_def {c : HasContext.Context (Proposition Atom)} :
+    c.fill φ = c<[φ] := rfl
 
 open scoped Proposition Proposition.Context
 
-instance : IsEquiv (Proposition Label) (Proposition.Equiv (State := State) (Label := Label)) where
-  refl := by grind
-  symm := by grind
-  trans := by grind
+/-- Logical equivalence is an equivalence relation. -/
+instance : IsEquiv (Proposition Label) (Proposition.Equiv lts) := by
+  rw [← equivalence_iff_isEquiv]
+  grind [Equivalence, Proposition.Equiv]
 
-instance {State : Type u} {Label : Type v} :
-    Congruence (Proposition Label) (Proposition.Equiv (State := State) (Label := Label)) where
-  elim :
-      Covariant (Proposition.Context Label) (Proposition Label) (Proposition.Context.fill)
-      Proposition.Equiv := by
-    intro ctx a b hab lts
-    specialize hab lts
+/-- Logical equivalence is a lawful congruence. -/
+instance (lts : LTS State Label) :
+    LawfulCongruence (Proposition.Equiv lts) where
+  elim ctx φ₁ φ₂ heqv := by
     induction ctx
-      <;> simp only [Proposition.Context.fill, Proposition.denotation]
-      <;> grind
-
-/-- Bundled version of a judgement for `Satisfy`. -/
-structure Satisfies.Judgement (State : Type u) (Label : Type v) where
-  /-- The state transition system to consider. -/
-  lts : LTS State Label
-  /-- The state to check the proposition against. -/
-  state : State
-  /-- The proposition to check. -/
-  φ : Proposition Label
-
-/-- `Satisfies` variant using bundled judgements. -/
-def Satisfies.Bundled (j : Satisfies.Judgement State Label) := Satisfies j.lts j.state j.φ
-
-instance : HasInferenceSystem (Satisfies.Judgement World Atom) := ⟨Satisfies.Bundled⟩
-
-@[scoped grind =]
-theorem Satisfies.bundled_char : Satisfies.Bundled j ↔ Satisfies j.lts j.state j.φ := by rfl
+    case hole =>
+      grind [=_ Proposition.Context.fill_def]
+    case not c ih | andL c ih | andR c ih =>
+      intro s
+      specialize ih s
+      grind [=_ Proposition.Context.fill_def]
+    case diamond c ih =>
+      intro s
+      rw [Satisfies.iff_iff_iff]
+      apply Iff.intro
+      all_goals
+        rintro ⟨w', h⟩
+        specialize ih w'
+        grind [=_ Proposition.Context.fill_def]
 
 /-- Judgemental contexts. -/
-structure Satisfies.Context (State : Type u) (Label : Type v) where
-  /-- The state transition system to consider. -/
+structure Judgement.Context State Label where
+  /-- The labelled transition system to consider. -/
   lts : LTS State Label
   /-- The state to check propositions against. -/
   state : State
 
 /-- Fills a judgemental context with a proposition. -/
-def Satisfies.Context.fill (c : Satisfies.Context State Label) (φ : Proposition Label) :
-    Satisfies.Judgement State Label where
+def Judgement.Context.fill (c : Judgement.Context State Label) (φ : Proposition Label) :
+    Judgement State Label where
   lts := c.lts
   state := c.state
   φ := φ
 
-instance judgementalContext :
-    HasHContext (Satisfies.Judgement State Label) (Proposition Label) :=
-  ⟨Satisfies.Context State Label, Satisfies.Context.fill⟩
-
-instance : HasLogicalEquivalence
-    (Proposition Label) (Satisfies.Judgement State Label) where
-  eqv := Proposition.Equiv
-  eqvFillValid {a b : Proposition Label} (heqv : a.Equiv (State := State) b)
-      (c : HasHContext.Context (Satisfies.Judgement State Label) (Proposition Label))
-      (h : Satisfies.Bundled c<[a]) : Satisfies.Bundled c<[b] := by
-    simp only [Satisfies.bundled_char, HasHContext.fill, Satisfies.Context.fill]
-    simp only [Satisfies.bundled_char, HasHContext.fill, Satisfies.Context.fill] at h
+instance : HasHContext (Judgement State Label) (Proposition Label) :=
+  ⟨Judgement.Context.fill⟩
+
+@[scoped grind =]
+lemma Judgement.Context.fill_def {c : Judgement.Context World Atom} {φ : Proposition Atom} :
+    HML[c.lts,c.state ⊨ φ] = c<[φ] := rfl
+
+/-- Universal logical equivalence: logical equivalence under all LTSs. -/
+def Proposition.UEquiv.{u, v} {Label : Type v} (φ₁ φ₂ : Proposition Label) : Prop :=
+  ∀ ⦃State : Type u⦄ (lts : LTS State Label), φ₁ ≡[Equiv lts] φ₂
+
+instance : DefaultCongruence (Proposition Label) (Proposition.UEquiv (Label := Label)) := ⟨⟩
+
+@[scoped grind =]
+theorem Proposition.uEquiv_def.{u, v} : UEquiv.{u, v} φ₁ φ₂ ↔ φ₁ ≡[UEquiv.{u, v}] φ₂ := by
+  simp [Congruence.r]
+
+@[scoped grind =]
+theorem Proposition.uEquiv_iff_forall_equiv.{u, v} {Label : Type v} (φ₁ φ₂ : Proposition Label) :
+    (φ₁ ≡[UEquiv.{u, v}] φ₂) ↔ ∀ {State : Type u} (lts : LTS State Label), φ₁ ≡[Equiv lts] φ₂ := by
+  rfl
+
+/-- Universal logical equivalence is an equivalence relation. -/
+instance : IsEquiv (Proposition Label) Proposition.UEquiv := by
+  rw [← equivalence_iff_isEquiv]
+  constructor
+  · intro φ State lts s
     grind
+  · intro φ₁ φ₂ h State lts s
+    grind [h lts]
+  · intro φ₁ φ₂ φ₃ h₁ h₂ State lts
+    grind [h₁ lts, h₂ lts, Proposition.forall_der_equiv lts]
+
+/-- Universal logical equivalence is a lawful congruence. -/
+instance {Label} : LawfulCongruence (Proposition.UEquiv (Label := Label)) where
+  elim :
+      Covariant (Proposition.Context Label) (Proposition Label) Proposition.Context.fill
+      Proposition.UEquiv := by
+    intro ctx φ₁ φ₂ h State lts
+    induction ctx <;> grind [h lts, Proposition.forall_der_equiv lts]
+
+instance : LogicalEquivalence (Judgement := Judgement State Label) InferenceSystem.Default
+    (Proposition.UEquiv (Label := Label)) where
+  eqvFillValid heqv c h := by
+    specialize heqv c.lts c.state
+    grind [=_ Judgement.Context.fill_def, HasHContext.fill, Judgement.Context.fill]
+
+end Theory
+
+section Equivalences
+
+/-! ## Database of logical equivalences -/
+
+namespace Proposition
+
+theorem false_and_false_eqv_false :
+    (⊥ ∧ ⊥ : Proposition Label) ≡ (⊥ : Proposition Label) := by
+  intro State lts
+  have := forall_der_equiv lts
+  grind
+
+/-- The dual axiom (reformulated for HML from modal logic). -/
+theorem dual (μ : Label) (φ : Proposition Label) :
+    (d⟨μ⟩φ) ≡ (¬d[μ]¬φ) := by
+  intro State lts s
+  grind
+
+end Proposition
+
+end Equivalences
 
 end Cslib.Logic.HML
diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean
index ce8db29a4..7a0aaeba3 100644
--- a/Cslib/Logics/LinearLogic/CLL/Basic.lean
+++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean
@@ -96,7 +96,7 @@ def Proposition.Context.fill (c : Context Atom) (a : Proposition Atom) : Proposi
   | bang c => .bang (c.fill a)
   | quest c => .quest (c.fill a)
 
-instance : HasContext (Proposition Atom) := ⟨Proposition.Context Atom, Proposition.Context.fill⟩
+instance : HasContext (Proposition Atom) := ⟨Proposition.Context.fill⟩
 
 /-- Definition of context filling. -/
 @[scoped grind =]
@@ -183,8 +183,7 @@ def Sequent.Context Atom := Sequent Atom
 /-- Filling a judgemental context returns a sequent. -/
 def Sequent.Context.fill (Γc : Sequent.Context Atom) (a : Proposition Atom) := a ::ₘ Γc
 
-instance : HasHContext (Sequent Atom) (Proposition Atom) :=
-  ⟨Sequent.Context Atom, Sequent.Context.fill⟩
+instance : HasHContext (Sequent Atom) (Proposition Atom) := ⟨Sequent.Context.fill⟩
 
 open Proposition in
 /-- A proof in the sequent calculus for classical linear logic. -/
@@ -259,8 +258,11 @@ open Sequent in
 def Proposition.Equiv (a b : Proposition Atom) :=
   Derivable ({a⫠, b} : Sequent Atom) ∧ Derivable ({b⫠, a} : Sequent Atom)
 
-@[inherit_doc]
-scoped infix:29 " ≡ " => Proposition.Equiv
+instance : DefaultCongruence (Proposition Atom) (Proposition.Equiv (Atom := Atom)) := ⟨⟩
+
+@[scoped grind =]
+theorem Proposition.prop_equiv_def {a b : Proposition Atom} : Proposition.Equiv a b ↔ a ≡ b := by
+  rfl
 
 /-- Conversion from proof-relevant to proof-irrelevant versions of propositional
 equivalence. -/
@@ -643,19 +645,16 @@ private lemma Proposition.equiv_quest {a a' : Proposition Atom} (h : a ≡ a') :
       apply Proof.quest
       apply h₂.rwConclusion (by grind)
 
-instance : Congruence (Proposition Atom) Proposition.Equiv where
+instance : LawfulCongruence (Proposition.Equiv (Atom := Atom)) where
   elim :
       Covariant (Proposition.Context Atom) (Proposition Atom) (Proposition.Context.fill)
       Proposition.Equiv := by
     intro ctx a b hab
     induction ctx <;> grind [= Context.fill]
 
-noncomputable instance : HasLogicalEquivalence (Proposition Atom) (Sequent Atom) where
-  eqv := Proposition.Equiv
-  eqvFillValid {a b : Proposition Atom} (heqv : a.Equiv b)
-      (c : HasHContext.Context (Sequent Atom) (Proposition Atom))
-      (h : ⇓c<[a]) : ⇓c<[b] := by
-    apply substEqvHead (chooseEquiv heqv) h
+noncomputable instance : LogicalEquivalence
+    (Judgement := Sequent Atom) InferenceSystem.Default (Proposition.Equiv (Atom := Atom)) where
+  eqvFillValid heqv _ h := substEqvHead (chooseEquiv heqv) h
 
 /-- Tensor is commutative. -/
 @[scoped grind ←]
diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index 0f34ad0e5..092ff00e6 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -29,26 +29,37 @@ def Proposition.Equiv (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition At
     : Prop :=
   ∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]
 
-@[inherit_doc]
-scoped notation φ₁ " ≡[" S "] " φ₂ => Proposition.Equiv S φ₁ φ₂
-
-@[inherit_doc]
-scoped notation φ₁ " ≡ " φ₂ => Proposition.Equiv Set.univ φ₁ φ₂
+instance : Congruence (Proposition.Equiv S) := ⟨⟩
 
 @[scoped grind =]
 theorem Proposition.equiv_def (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) :
-    (φ₁ ≡[S] φ₂) ↔
-    (∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) := by rfl
-
-@[scoped grind =]
-theorem Proposition.equiv_iff (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) :
-    (φ₁ ≡[S] φ₂) ↔
-    (∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by
-  simp [Proposition.equiv_def, Satisfies.iff_iff_iff]
-
+    φ₁.Equiv S φ₂ ↔ (φ₁ ≡[Equiv S] φ₂) := by rfl
+
+@[scoped grind ⇒]
+theorem Proposition.equiv_forall_der (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom)
+    (h : φ₁ ≡[Equiv S] φ₂) : ∀ m ∈ S, ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] := by
+  intro s
+  specialize h s
+  assumption
+
+theorem Proposition.forall_der_equiv (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom)
+    (h : ∀ m ∈ S, ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) : φ₁ ≡[Equiv S] φ₂ := by
+  intro s
+  specialize h s
+  assumption
+
+@[scoped grind ⇒]
+theorem Proposition.equiv_iff (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom)
+    (h : φ₁ ≡[Equiv S] φ₂) (m : Model World Atom) (hm : m ∈ S) (w : World) :
+    ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂] := by
+  grind [=_ Satisfies.iff_iff_iff]
+
+/-- Logical equivalence preserves validity. -/
 theorem Proposition.equiv_valid (S : Set (Model World Atom))
-    (φ₁ φ₂ : Proposition Atom) (h : φ₁ ≡[S] φ₂) :
+    (φ₁ φ₂ : Proposition Atom) (h : φ₁ ≡[Equiv S] φ₂) :
     (φ₁.valid S ↔ φ₂.valid S) := by
+  apply Proposition.equiv_forall_der at h
+  simp only [Satisfies.iff_iff_iff] at h
   grind
 
 /-- Propositional contexts. -/
@@ -69,11 +80,11 @@ def Proposition.Context.fill (c : Context Atom) (φ : Proposition Atom) :=
   | andR φ' c => φ'.and (c.fill φ)
   | diamond c => .diamond (c.fill φ)
 
-instance : HasContext (Proposition Atom) := ⟨Proposition.Context Atom, Proposition.Context.fill⟩
+instance : HasContext (Proposition Atom) := ⟨Proposition.Context.fill⟩
 
-@[scoped grind =_]
-lemma Proposition.Context.fill_def {Γ : HasContext.Context (Proposition Atom)} :
-    Γ.fill φ = Γ<[φ] := rfl
+@[scoped grind =]
+lemma Proposition.Context.fill_def {c : HasContext.Context (Proposition Atom)} :
+    c.fill φ = c<[φ] := rfl
 
 open scoped Proposition Proposition.Context
 
@@ -81,24 +92,24 @@ open scoped Proposition Proposition.Context
 instance {World Atom} (S : Set (Model World Atom)) :
     IsEquiv (Proposition Atom) (Proposition.Equiv S) := by
   rw [← equivalence_iff_isEquiv]
-  grind [Equivalence]
+  grind [Equivalence, Proposition.Equiv]
 
 /-- Logical equivalence is a congruence. -/
 instance {World Atom} (S : Set (Model World Atom)) :
-    Congruence (Proposition Atom) (Proposition.Equiv S) where
+    LawfulCongruence (Proposition.Equiv S) where
   elim ctx φ₁ φ₂ heqv m hₘ w := by
     induction ctx generalizing w
-    case hole => grind
+    case hole => grind [=_ Proposition.Context.fill_def]
     case not c ih | andL c ih | andR c ih =>
       specialize ih w
-      grind
+      grind [=_ Proposition.Context.fill_def]
     case diamond c ih =>
       rw [Satisfies.iff_iff_iff]
       apply Iff.intro
       all_goals
         rintro ⟨w', h⟩
         specialize ih w'
-        grind
+        grind [=_ Proposition.Context.fill_def]
 
 /-- Judgemental contexts. -/
 structure Satisfies.Context (World Atom : Type*) where
@@ -111,22 +122,22 @@ structure Satisfies.Context (World Atom : Type*) where
 def Satisfies.Context.fill (c : Satisfies.Context World Atom) (φ : Proposition Atom) :
     Judgement World Atom := Modal[c.m, c.w ⊨ φ]
 
-instance judgementalContext :
-    HasHContext (Judgement World Atom) (Proposition Atom) :=
-  ⟨Satisfies.Context World Atom, Satisfies.Context.fill⟩
+instance : HasHContext (Judgement World Atom) (Proposition Atom) :=
+  ⟨Satisfies.Context.fill⟩
 
-@[scoped grind =_]
+@[scoped grind =]
 lemma Satisfies.Context.fill_def {c : Satisfies.Context World Atom} :
     Modal[c.m,c.w ⊨ φ] = c<[φ] := rfl
 
 open scoped Satisfies.Context
 
 /-- Logical equivalence for Modal Logic K. That is, no assumptions on models are made. -/
-instance : HasLogicalEquivalence
-    (Proposition Atom) (Judgement World Atom) where
-  eqv := Proposition.Equiv Set.univ
+instance : LogicalEquivalence
+    (α := Proposition Atom)
+    (Judgement := Judgement World Atom) InferenceSystem.Default
+    (Proposition.Equiv (Set.univ (α := Model World Atom))) where
   eqvFillValid heqv c h := by
     specialize heqv c.m
-    grind
+    grind [=_ Satisfies.Context.fill_def]
 
 end Cslib.Logic.Modal
diff --git a/CslibTests.lean b/CslibTests.lean
index 8bc051b31..99f1d31f5 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -1,6 +1,7 @@
 import CslibTests.Bisimulation
 import CslibTests.CCS
 import CslibTests.CLL
+import CslibTests.Congruence
 import CslibTests.DFA
 import CslibTests.FreeMonad
 import CslibTests.GrindLint
@@ -9,6 +10,7 @@ import CslibTests.HasFresh
 import CslibTests.HasSubstitution
 import CslibTests.HasWellFormed
 import CslibTests.ImportWithMathlib
+import CslibTests.InferenceSystem
 import CslibTests.LTS
 import CslibTests.LambdaCalculus
 import CslibTests.MLL
diff --git a/CslibTests/CLL.lean b/CslibTests/CLL.lean
index 55f15b98f..3355b0ab1 100644
--- a/CslibTests/CLL.lean
+++ b/CslibTests/CLL.lean
@@ -13,6 +13,7 @@ namespace CslibTests
 I use `Proposition Nat` as the concrete instantiation for atoms.
 -/
 
+open Cslib
 open Cslib.Logic.CLL
 
 /-! ## Proposition construction tests -/
diff --git a/CslibTests/Congruence.lean b/CslibTests/Congruence.lean
new file mode 100644
index 000000000..f28de54d3
--- /dev/null
+++ b/CslibTests/Congruence.lean
@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Foundations.Syntax.Congruence
+
+namespace CslibTests
+
+open Cslib
+
+def myRel (n m : ℕ) := n = m
+
+instance : DefaultCongruence ℕ myRel := ⟨⟩
+
+example : (2 : ℕ) ≡ (2 : ℕ) := by rfl
+example : (2 : ℕ) ≡[myRel] (2 : ℕ) := by rfl
+
+end CslibTests
diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean
index deba30056..ebc811861 100644
--- a/CslibTests/GrindLint.lean
+++ b/CslibTests/GrindLint.lean
@@ -70,7 +70,6 @@ open_scoped_all Cslib
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.sub
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.ty
 #grind_lint skip Cslib.Logic.HML.bisimulation_satisfies
-#grind_lint skip Cslib.Logic.HML.Satisfies.diamond
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.step_multiApp_l
 #adaptation_note
 /-- (changes from lean#13166) -/
diff --git a/CslibTests/HML.lean b/CslibTests/HML.lean
index 3e9346f2b..b1a4fae2f 100644
--- a/CslibTests/HML.lean
+++ b/CslibTests/HML.lean
@@ -5,15 +5,43 @@ Authors: Fabrizio Montesi
 -/
 
 import Cslib.Logics.HML.Basic
+import Cslib.Logics.HML.LogicalEquivalence
 import Cslib.Languages.CCS.Semantics
 
 namespace CslibTests
 
-open Cslib
-open CCS Logic.HML LTS
+open Cslib Logic HML LTS
 
 example [∀ p μ, Finite ((CCS.lts (defs := defs)).image p μ)] :
     TheoryEq (CCS.lts (defs := defs)) = HomBisimilarity (CCS.lts (defs := defs)) :=
   theoryEq_eq_bisimilarity ..
 
+section LogicalEquivalence
+
+/-
+The next example tests that logical equivalence can lift equivalences.
+
+We prove it twice. Once using our infrastructure for up-to context reasoning directly, and then
+with grind. Note that the grind proof works because Satisfies.and_iff_and gives a congruence
+principle on the satisfaction relation for the and-connective.
+-/
+
+open scoped InferenceSystem
+open Proposition
+
+example {State : Type u} {lts : LTS State Label} {s : State} {μ : Label} {φ₁ φ₂ : Proposition Label}
+    (h : ⇓HML[lts,s ⊨ (d⟨μ⟩φ₁) ∧ φ₂])
+    : ⇓HML[lts,s ⊨ (¬d[μ]¬φ₁) ∧ φ₂] := by
+  let pc : HasContext.Context (Proposition Label) := Context.andL .hole φ₂
+  have eqv := LawfulCongruence.covariant.elim pc (dual μ φ₁)
+  let jc : HasHContext.Context (Judgement State Label) (Proposition Label) :=
+    Judgement.Context.mk lts s
+  apply LogicalEquivalence.eqvFillValid eqv jc h
+
+example {State : Type u} {lts : LTS State Label} {s : State} {μ : Label} {φ₁ φ₂ : Proposition Label}
+    (h : ⇓HML[lts,s ⊨ (d⟨μ⟩φ₁) ∧ φ₂]) : ⇓HML[lts,s ⊨ (¬d[μ]¬φ₁) ∧ φ₂] := by
+  grind only [= Satisfies.and_iff_and, => equiv_iff, dual μ φ₁ lts]
+
+end LogicalEquivalence
+
 end CslibTests
diff --git a/CslibTests/InferenceSystem.lean b/CslibTests/InferenceSystem.lean
new file mode 100644
index 000000000..43bd6a952
--- /dev/null
+++ b/CslibTests/InferenceSystem.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Foundations.Logic.InferenceSystem
+
+namespace CslibTests
+
+open Cslib.Logic
+
+instance : HasInferenceSystem ℕ := ⟨fun _ => True⟩
+
+open scoped InferenceSystem
+
+-- Tests that the delaboration of `InferenceSystem.Default` in the `⇓` notation works.
+
+/-- info: ⇓5 : Prop -/
+#guard_msgs in
+#check ⇓5
+
+example : ⇓5 := by dsimp [InferenceSystem.derivation]
+
+end CslibTests