diff --git a/Cslib.lean b/Cslib.lean
index a9d5ffc3e..fcb0b0a8b 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -54,6 +54,8 @@ public import Cslib.Foundations.Data.Relation
 public import Cslib.Foundations.Data.Set.Saturation
 public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
+public import Cslib.Foundations.Logic.InferenceSystem
+public import Cslib.Foundations.Logic.LogicalEquivalence
 public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
 public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
@@ -94,6 +96,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
 public import Cslib.Logics.HML.Basic
+public import Cslib.Logics.HML.LogicalEquivalence
 public import Cslib.Logics.LinearLogic.CLL.Basic
 public import Cslib.Logics.LinearLogic.CLL.CutElimination
 public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
diff --git a/Cslib/Foundations/Logic/InferenceSystem.lean b/Cslib/Foundations/Logic/InferenceSystem.lean
new file mode 100644
index 000000000..3a9eda6f1
--- /dev/null
+++ b/Cslib/Foundations/Logic/InferenceSystem.lean
@@ -0,0 +1,52 @@
+/-
+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.Logic
+
+/--
+The notation typeclass for inference systems.
+This enables the notation `⇓a`, where `a : α` is a derivable value.
+-/
+class InferenceSystem (α : Type u) where
+  /--
+  `⇓a` is a derivation of `a`, that is, a witness that `a` is derivable.
+  The meaning of this notation is type-dependent.
+  -/
+  derivation (s : α) : Sort v
+
+namespace InferenceSystem
+
+@[inherit_doc] scoped notation "⇓" a:90 => InferenceSystem.derivation a
+
+/-- Rewrites the conclusion of a proof into an equal one. -/
+@[scoped grind =]
+def rwConclusion [InferenceSystem α] {Γ Δ : α} (h : Γ = Δ) (p : ⇓Γ) : ⇓Δ := h ▸ p
+
+/-- `a` is derivable if it is the conclusion of some derivation. -/
+def Derivable [InferenceSystem α] (a : α) := Nonempty (⇓a)
+
+/-- Shows derivability from a derivation. -/
+theorem Derivable.fromDerivation [InferenceSystem α] {a : α} (d : ⇓a) : Derivable a :=
+  Nonempty.intro d
+
+instance [InferenceSystem α] {a : α} : Coe (⇓a) (Derivable a) := ⟨Derivable.fromDerivation⟩
+
+/-- Extracts (noncomputably) a derivation from the fact that a conclusion is derivable. -/
+noncomputable def Derivable.toDerivation [InferenceSystem α] {a : α} (d : Derivable a) : ⇓a :=
+  Classical.choice d
+
+noncomputable instance [InferenceSystem α] {a : α} : Coe (Derivable a) (⇓a) :=
+  ⟨Derivable.toDerivation⟩
+
+end InferenceSystem
+
+end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/LogicalEquivalence.lean b/Cslib/Foundations/Logic/LogicalEquivalence.lean
new file mode 100644
index 000000000..d24628559
--- /dev/null
+++ b/Cslib/Foundations/Logic/LogicalEquivalence.lean
@@ -0,0 +1,33 @@
+/-
+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.Syntax.Context
+public import Cslib.Foundations.Syntax.Congruence
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- 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
+    (Proposition : Type u) [HasContext Proposition]
+    (Judgement : Type v) [HasHContext Judgement Proposition]
+    (Valid : Judgement → Sort w) where
+  /-- The logical equivalence relation. -/
+  eqv (a b : Proposition) : Prop
+  /-- Proof that `eqv` is a congruence. -/
+  [congruence : Congruence Proposition eqv]
+  /-- Validity is preserved for any judgemental context. -/
+  eqv_fill_valid (heqv : eqv a b) (c : HasHContext.Context Judgement Proposition)
+    (h : Valid (c<[a])) : Valid (c<[b])
+
+@[inherit_doc]
+scoped infix:29 " ≡ " => LogicalEquivalence.eqv
+
+end Cslib.Logic
diff --git a/Cslib/Foundations/Syntax/Congruence.lean b/Cslib/Foundations/Syntax/Congruence.lean
index 0e710b147..b32ab53e9 100644
--- a/Cslib/Foundations/Syntax/Congruence.lean
+++ b/Cslib/Foundations/Syntax/Congruence.lean
@@ -13,7 +13,7 @@ public import Mathlib.Algebra.Order.Monoid.Unbundled.Defs
 
 namespace Cslib
 
-/-- An equivalence relation preserved by all contexts. -/
+/-- An equivalence relation on `α` preserved by all contexts `Ctx`. -/
 class Congruence (α : Type*) [HasContext α] (r : α → α → Prop) extends
   IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) r
 
diff --git a/Cslib/Foundations/Syntax/Context.lean b/Cslib/Foundations/Syntax/Context.lean
index d4ae23789..bff8f952f 100644
--- a/Cslib/Foundations/Syntax/Context.lean
+++ b/Cslib/Foundations/Syntax/Context.lean
@@ -12,13 +12,20 @@ public import Cslib.Init
 
 namespace Cslib
 
-/-- Class for types (`Term`) that have a notion of (single-hole) contexts (`Context`). -/
-class HasContext (Term : Sort*) where
+/-- Class for types with a canonical notion of heterogeneous single-hole contexts. -/
+class HasHContext (α β : Type*) where
   /-- The type of contexts. -/
-  Context : Sort*
-  /-- Replaces the hole in the context with a term. -/
-  fill (c : Context) (t : Term) : Term
+  Context : Type*
+  /-- Replaces the hole in the context with a value, resulting in a new value. -/
+  fill (c : Context) (b : β) : α
 
-@[inherit_doc] notation:max c "<[" t "]" => HasContext.fill c t
+@[inherit_doc] notation:max c "<[" t "]" => HasHContext.fill c t
+
+/-- Class for types (`α`) that have a canonical notion of homogeneous single-hole contexts
+(`Context`). -/
+abbrev HasContext (α : Type*) := HasHContext α α
+
+@[inherit_doc HasHContext.Context]
+def HasContext.Context (α : Type*) [HasContext α] : Type* := HasHContext.Context α α
 
 end Cslib
diff --git a/Cslib/Languages/CCS/Basic.lean b/Cslib/Languages/CCS/Basic.lean
index 1c3a71ef7..54fe7181a 100644
--- a/Cslib/Languages/CCS/Basic.lean
+++ b/Cslib/Languages/CCS/Basic.lean
@@ -123,14 +123,14 @@ instance : HasContext (Process Name Constant) := ⟨Context Name Constant, Conte
 
 /-- Definition of context filling. -/
 @[scoped grind =]
-theorem hasContext_def (c : Context Name Constant) (p : Process Name Constant) :
+theorem context_fill_def (c : Context Name Constant) (p : Process Name Constant) :
   c<[p] = c.fill p := rfl
 
 /-- Any `Process` can be obtained by filling a `Context` with an atom. This proves that `Context`
 is a complete formalisation of syntactic contexts for CCS. -/
 theorem Context.complete (p : Process Name Constant) :
-    ∃ c : Context Name Constant, p = c<[Process.nil] ∨
-    ∃ k : Constant, p = c<[Process.const k] := by
+    ∃ c : Context Name Constant, p = c<[(Process.nil : Process Name Constant)] ∨
+    ∃ k : Constant, p = c<[(Process.const k : Process Name Constant)] := by
   induction p
   case nil =>
     exists hole
diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean
new file mode 100644
index 000000000..a82181134
--- /dev/null
+++ b/Cslib/Logics/HML/LogicalEquivalence.lean
@@ -0,0 +1,115 @@
+/-
+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.Logics.HML.Basic
+public import Cslib.Foundations.Logic.LogicalEquivalence
+
+@[expose] public section
+
+/-! # Logical Equivalence in HML
+
+This module defines logical equivalence for HML propositions and instantiates `LogicalEquivalence`.
+-/
+
+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
+
+@[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
+
+/-- 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)
+  | diamond (μ : Label) (c : Context Label)
+  | box (μ : Label) (c : Context Label)
+
+/-- Replaces a hole in a propositional context with a proposition. -/
+@[scoped grind =]
+def Proposition.Context.fill (c : Context Label) (φ : Proposition Label) :=
+  match c with
+  | hole => φ
+  | andL c φ' => (c.fill φ).and φ'
+  | andR φ' c => φ'.and (c.fill φ)
+  | orL c φ' => (c.fill φ).or φ'
+  | orR φ' c => φ'.or (c.fill φ)
+  | diamond μ c => .diamond μ (c.fill φ)
+  | box μ c => .box μ (c.fill φ)
+
+instance : HasContext (Proposition Label) := ⟨Proposition.Context Label, Proposition.Context.fill⟩
+
+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
+
+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
+    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.φ
+
+@[scoped grind =]
+theorem Satisfies.bundled_char : Satisfies.Bundled j ↔ Satisfies j.lts j.state j.φ := by rfl
+
+/-- Judgemental contexts. -/
+structure Satisfies.Context (State : Type u) (Label : Type v) where
+  /-- The state 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
+  lts := c.lts
+  state := c.state
+  φ := φ
+
+instance judgementalContext :
+    HasHContext (Satisfies.Judgement State Label) (Proposition Label) :=
+  ⟨Satisfies.Context State Label, Satisfies.Context.fill⟩
+
+instance : LogicalEquivalence
+    (Proposition Label) (Satisfies.Judgement State Label) (Satisfies.Bundled) where
+  eqv := Proposition.Equiv
+  eqv_fill_valid {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
+    grind
+
+end Cslib.Logic.HML
diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean
index c7cb4558e..a429d112f 100644
--- a/Cslib/Logics/LinearLogic/CLL/Basic.lean
+++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean
@@ -7,6 +7,9 @@ Authors: Fabrizio Montesi
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Syntax.Context
+public import Cslib.Foundations.Logic.InferenceSystem
+public import Cslib.Foundations.Logic.LogicalEquivalence
 public import Mathlib.Data.Multiset.Fold
 
 @[expose] public section
@@ -68,6 +71,44 @@ instance : Bot (Proposition Atom) := ⟨.bot⟩
 @[inherit_doc] scoped prefix:95 "!" => Proposition.bang
 @[inherit_doc] scoped prefix:95 "ʔ" => Proposition.quest
 
+/-- Propositional contexts (single-hole contexts for propositions). -/
+inductive Proposition.Context (Atom : Type u) : Type u where
+  | hole
+  | tensorL (c : Context Atom) (b : Proposition Atom)
+  | tensorR (a : Proposition Atom) (c : Context Atom)
+  | parrL (c : Context Atom) (b : Proposition Atom)
+  | parrR (a : Proposition Atom) (c : Context Atom)
+  | oplusL (c : Context Atom) (b : Proposition Atom)
+  | oplusR (a : Proposition Atom) (c : Context Atom)
+  | withL (c : Context Atom) (b : Proposition Atom)
+  | withR (a : Proposition Atom) (c : Context Atom)
+  | bang (c : Context Atom)
+  | quest (c : Context Atom)
+deriving DecidableEq, BEq
+
+/-- Replaces the hole in a propositional context with a propositions. -/
+@[scoped grind =]
+def Proposition.Context.fill (c : Context Atom) (a : Proposition Atom) : Proposition Atom :=
+  match c with
+  | hole => a
+  | tensorL c b => .tensor (c.fill a) b
+  | tensorR b c => .tensor b (c.fill a)
+  | parrL c b => .parr (c.fill a) b
+  | parrR b c => .parr b (c.fill a)
+  | oplusL c b => .oplus (c.fill a) b
+  | oplusR b c => .oplus b (c.fill a)
+  | withL c b => .with (c.fill a) b
+  | withR b c => .with b (c.fill a)
+  | bang c => .bang (c.fill a)
+  | quest c => .quest (c.fill a)
+
+instance : HasContext (Proposition Atom) := ⟨Proposition.Context Atom, Proposition.Context.fill⟩
+
+/-- Definition of context filling. -/
+@[scoped grind =]
+theorem Proposition.context_fill_def (c : Context Atom) (a : Proposition Atom) :
+  c<[a] = c.fill a := rfl
+
 /-- Positive propositions. -/
 def Proposition.positive : Proposition Atom → Bool
   | atom _ => true
@@ -152,6 +193,15 @@ def Sequent.allQuest (Γ : Sequent Atom) :=
   Γ.map (· matches ʔ_)
   |> Multiset.fold Bool.and true
 
+/-- Judgemental contexts for CLL. -/
+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⟩
+
 open Proposition in
 /-- A proof in the sequent calculus for classical linear logic. -/
 inductive Proof : Sequent Atom → Type u where
@@ -171,34 +221,19 @@ inductive Proof : Sequent Atom → Type u where
   | bang {Γ : Sequent Atom} {a} : Γ.allQuest → Proof (a ::ₘ Γ) → Proof ((!a) ::ₘ Γ)
   -- No rule for zero.
 
-@[inherit_doc]
-scoped notation "⇓" Γ:90 => Proof Γ
-
-/-- Rewrites the conclusion of a proof into an equal one. -/
-@[scoped grind =]
-def Proof.rwConclusion (h : Γ = Δ) (p : ⇓Γ) : ⇓Δ := h ▸ p
+open Logic
 
-/-- A sequent is provable if there exists a proof that concludes it. -/
-@[scoped grind =]
-def Sequent.Provable (Γ : Sequent Atom) := Nonempty (⇓Γ)
+instance : InferenceSystem (Sequent Atom) := ⟨Proof⟩
 
-/-- Having a proof of Γ shows that it is provable. -/
-theorem Sequent.Provable.fromProof {Γ : Sequent Atom} (p : ⇓Γ) : Γ.Provable := ⟨p⟩
+open InferenceSystem
 
-/-- Having a proof of Γ shows that it is provable. -/
+/-- Convenience definition for rewriting conclusions in proofs. -/
 @[scoped grind =]
-noncomputable def Sequent.Provable.toProof {Γ : Sequent Atom} (p : Γ.Provable) : ⇓Γ :=
-  Classical.choice p
-
-instance : Coe (Proof Γ) (Γ.Provable) where
-  coe p := Sequent.Provable.fromProof p
-
-noncomputable instance : Coe (Γ.Provable) (Proof Γ) where
-  coe p := p.toProof
+def Proof.rwConclusion {Γ Δ : Sequent Atom} (h : Γ = Δ) (p : ⇓Γ) := InferenceSystem.rwConclusion h p
 
 /-- The axiom, but where the order of propositions is reversed. -/
 @[scoped grind <=]
-def Proof.ax' {a : Proposition Atom} : ⇓{a⫠, a} :=
+def Proof.ax' {a : Proposition Atom} : ⇓({a⫠, a} : Sequent Atom) :=
   Multiset.pair_comm a (a⫠) ▸ Proof.ax
 
 /-- Cut, but where the premises are reversed. -/
@@ -235,27 +270,29 @@ section LogicalEquiv
 
 /-- Two propositions are equivalent if one implies the other and vice versa.
 Proof-relevant version. -/
-def Proposition.equiv (a b : Proposition Atom) := ⇓{a⫠, b} × ⇓{b⫠, a}
-
-open Sequent in
-/-- Propositional equivalence, proof-irrelevant version (`Prop`). -/
-def Proposition.Equiv (a b : Proposition Atom) := Provable {a⫠, b} ∧ Provable {b⫠, a}
-
-/-- Conversion from proof-relevant to proof-irrelevant versions of propositional
-equivalence. -/
-theorem Proposition.equiv.toProp (h : Proposition.equiv a b) : Proposition.Equiv a b := by
-  obtain ⟨p, q⟩ := h
-  exact ⟨p, q⟩
+def Proposition.equiv (a b : Proposition Atom) :=
+  ⇓({a⫠, b} : Sequent Atom) × ⇓({b⫠, a} : Sequent Atom)
 
 @[inherit_doc]
 scoped infix:29 " ≡⇓ " => Proposition.equiv
 
+open Sequent in
+/-- Propositional equivalence, proof-irrelevant version (`Prop`). -/
+def Proposition.Equiv (a b : Proposition Atom) :=
+  Derivable ({a⫠, b} : Sequent Atom) ∧ Derivable ({b⫠, a} : Sequent Atom)
+
 @[inherit_doc]
 scoped infix:29 " ≡ " => Proposition.Equiv
 
+/-- Conversion from proof-relevant to proof-irrelevant versions of propositional
+equivalence. -/
+theorem Proposition.equiv.toProp (h : a ≡⇓ b) : a ≡ b := ⟨h.1, h.2⟩
+
 /-- Proof-relevant equivalence is coerciable into proof-irrelevant equivalence. -/
-instance {a b : Proposition Atom} : Coe (a ≡⇓ b) (a ≡ b) where
-  coe := Proposition.equiv.toProp
+instance : Coe (a ≡⇓ b) (a ≡ b) := ⟨Proposition.equiv.toProp⟩
+
+/-- Transforms a proof-irrelevant equivalence into a proof-relevant one (this is not computable). -/
+noncomputable def chooseEquiv (h : a ≡ b) : a ≡⇓ b := ⟨h.1, h.2⟩
 
 namespace Proposition
 
@@ -263,8 +300,7 @@ open Sequent
 
 /-- Proof-relevant equivalence is reflexive. -/
 @[scoped grind =]
-def equiv.refl (a : Proposition Atom) : a.equiv a :=
-  ⟨Proof.ax', Proof.ax'⟩
+def equiv.refl (a : Proposition Atom) : a ≡⇓ a := ⟨Proof.ax', Proof.ax'⟩
 
 /-- Proof-relevant equivalence is symmetric. -/
 @[scoped grind =]
@@ -287,21 +323,17 @@ theorem Equiv.symm {a b : Proposition Atom} (h : a ≡ b) : b ≡ a := ⟨h.2, h
 /-- Proof-irrelevant equivalence is transitive. -/
 @[scoped grind →]
 theorem Equiv.trans {a b c : Proposition Atom} (hab : a ≡ b) (hbc : b ≡ c) : a ≡ c :=
-  ⟨
-    Provable.fromProof
-      (Proof.cut (hab.1.toProof.rwConclusion (Multiset.pair_comm _ _)) hbc.1.toProof),
-    Provable.fromProof
-      (Proof.cut (hbc.2.toProof.rwConclusion (Multiset.pair_comm _ _)) hab.2.toProof)
-  ⟩
-
-/-- Transforms a proof-irrelevant equivalence into a proof-relevant one (this is not computable). -/
-noncomputable def chooseEquiv (h : a ≡ b) : a ≡⇓ b :=
-  ⟨h.1.toProof, h.2.toProof⟩
+  equiv.trans (chooseEquiv hab) (chooseEquiv hbc)
 
 /-- The canonical equivalence relation for propositions. -/
 def propositionSetoid : Setoid (Proposition Atom) :=
   ⟨Equiv, Equiv.refl, Equiv.symm, Equiv.trans⟩
 
+instance : IsEquiv (Proposition Atom) Proposition.Equiv where
+  refl := Equiv.refl
+  symm a b := Equiv.symm (a := a) (b := b)
+  trans a b c := Equiv.trans (a := a) (b := b) (c := c)
+
 /-- !⊤ ≡⇓ 1 -/
 @[scoped grind =]
 def bang_top_eqv_one : (!⊤ : Proposition Atom) ≡⇓ 1 :=
@@ -310,8 +342,8 @@ def bang_top_eqv_one : (!⊤ : Proposition Atom) ≡⇓ 1 :=
 /-- ʔ0 ≡⇓ ⊥ -/
 @[scoped grind =]
 def quest_zero_eqv_bot : (ʔ0 : Proposition Atom) ≡⇓ ⊥ :=
-  ⟨.rwConclusion (Multiset.pair_comm ..) <| .bot (.bang rfl .top),
-   .rwConclusion (Multiset.pair_comm ..) <| .weaken .one⟩
+  ⟨rwConclusion (Multiset.pair_comm ..) <| .bot (.bang rfl .top),
+   rwConclusion (Multiset.pair_comm ..) <| .weaken .one⟩
 
 /-- a ⊗ 0 ≡⇓ 0 -/
 @[scoped grind =]
@@ -366,6 +398,288 @@ open scoped Multiset in
 def subst_eqv {Γ Δ : Sequent Atom} (heqv : a ≡⇓ b) (p : ⇓(Γ + {a} + Δ)) : ⇓(Γ + {b} + Δ) :=
   add_middle_eq_cons ▸ subst_eqv_head heqv (add_middle_eq_cons ▸ p)
 
+open scoped Context
+
+@[local grind .]
+private lemma Proposition.equiv_tensor₁ {a a' b : Proposition Atom} (h : a ≡ a') :
+    a ⊗ b ≡ a' ⊗ b := by
+  obtain ⟨h₁, h₂⟩ := h
+  obtain h₁ := h₁.some
+  obtain h₂ := h₂.some
+  constructor
+  case left =>
+    constructor
+    simp only [Proposition.dual]
+    apply Proof.parr
+    rw [show (a⫠ ::ₘ b⫠ ::ₘ {a' ⊗ b}) = ((a' ⊗ b) ::ₘ ({a⫠} + {b⫠})) by grind]
+    apply Proof.tensor
+    · apply h₁.rwConclusion (by grind)
+    · exact Proof.ax
+  case right =>
+    constructor
+    simp only [Proposition.dual]
+    apply Proof.parr
+    rw [show (a'⫠ ::ₘ b⫠ ::ₘ {a ⊗ b}) = ((a ⊗ b) ::ₘ ({a'⫠} + {b⫠})) by grind]
+    apply Proof.tensor
+    · apply h₂.rwConclusion (by grind)
+    · exact Proof.ax
+
+@[local grind .]
+private lemma Proposition.equiv_tensor₂ {a b b' : Proposition Atom} (h : b ≡ b') :
+    a ⊗ b ≡ a ⊗ b' := by
+  obtain ⟨h₁, h₂⟩ := h
+  obtain h₁ := h₁.some
+  obtain h₂ := h₂.some
+  constructor
+  case left =>
+    constructor
+    simp only [Proposition.dual]
+    apply Proof.parr
+    rw [show (a⫠ ::ₘ b⫠ ::ₘ {a ⊗ b'}) = ((a ⊗ b') ::ₘ ({a⫠} + {b⫠})) by grind]
+    apply Proof.tensor
+    · exact Proof.ax
+    · apply h₁.rwConclusion (by grind)
+  case right =>
+    constructor
+    simp only [Proposition.dual]
+    apply Proof.parr
+    rw [show (a⫠ ::ₘ b'⫠ ::ₘ {a ⊗ b}) = ((a ⊗ b) ::ₘ ({a⫠} + {b'⫠})) by grind]
+    apply Proof.tensor
+    · exact Proof.ax
+    · apply h₂.rwConclusion (by grind)
+
+@[local grind .]
+private lemma Proposition.equiv_parr₁ {a a' b : Proposition Atom} (h : a ≡ a') :
+    a ⅋ b ≡ a' ⅋ b := by
+  obtain ⟨h₁, h₂⟩ := h
+  obtain h₁ := h₁.some
+  obtain h₂ := h₂.some
+  constructor
+  case left =>
+    constructor
+    simp only [Proposition.dual]
+    rw [show {a⫠ ⊗ b⫠, a' ⅋ b} = (a' ⅋ b) ::ₘ {a⫠ ⊗ b⫠} by grind]
+    apply Proof.parr
+    rw [show (a' ::ₘ b ::ₘ {a⫠ ⊗ b⫠}) = ((a⫠ ⊗ b⫠) ::ₘ ({a'} + {b})) by grind]
+    apply Proof.tensor
+    · apply h₁.rwConclusion (by grind)
+    · exact Proof.ax'
+  case right =>
+    constructor
+    simp only [Proposition.dual]
+    rw [show {a'⫠ ⊗ b⫠, a ⅋ b} = (a ⅋ b) ::ₘ {a'⫠ ⊗ b⫠} by grind]
+    apply Proof.parr
+    rw [show (a ::ₘ b ::ₘ {a'⫠ ⊗ b⫠}) = ((a'⫠ ⊗ b⫠) ::ₘ ({a} + {b})) by grind]
+    apply Proof.tensor
+    · apply h₂.rwConclusion (by grind)
+    · exact Proof.ax'
+
+@[local grind .]
+private lemma Proposition.equiv_parr₂ {a b b' : Proposition Atom} (h : b ≡ b') :
+    a ⅋ b ≡ a ⅋ b' := by
+  obtain ⟨h₁, h₂⟩ := h
+  obtain h₁ := h₁.some
+  obtain h₂ := h₂.some
+  constructor
+  case left =>
+    constructor
+    simp only [Proposition.dual]
+    rw [show {a⫠ ⊗ b⫠, a ⅋ b'} = (a ⅋ b') ::ₘ {a⫠ ⊗ b⫠} by grind]
+    apply Proof.parr
+    rw [show (a ::ₘ b' ::ₘ {a⫠ ⊗ b⫠}) = ((a⫠ ⊗ b⫠) ::ₘ ({a} + {b'})) by grind]
+    apply Proof.tensor
+    · exact Proof.ax'
+    · apply h₁.rwConclusion (by grind)
+  case right =>
+    constructor
+    simp only [Proposition.dual]
+    rw [show {a⫠ ⊗ b'⫠, a ⅋ b} = (a ⅋ b) ::ₘ {a⫠ ⊗ b'⫠} by grind]
+    apply Proof.parr
+    rw [show (a ::ₘ b ::ₘ {a⫠ ⊗ b'⫠}) = ((a⫠ ⊗ b'⫠) ::ₘ ({a} + {b})) by grind]
+    apply Proof.tensor
+    · exact Proof.ax'
+    · apply h₂.rwConclusion (by grind)
+
+@[local grind .]
+private lemma Proposition.equiv_oplus₁ {a a' b : Proposition Atom} (h : a ≡ a') :
+    a ⊕ b ≡ a' ⊕ b := by
+  obtain ⟨h₁, h₂⟩ := h
+  obtain h₁ := h₁.some
+  obtain h₂ := h₂.some
+  constructor
+  case left =>
+    constructor
+    simp only [Proposition.dual]
+    apply Proof.with
+    · rw [show a⫠ ::ₘ {a' ⊕ b} = (a' ⊕ b) ::ₘ {a⫠} by grind]
+      apply Proof.oplus₁
+      apply h₁.rwConclusion (by grind)
+    · rw [show b⫠ ::ₘ {a' ⊕ b} = (a' ⊕ b) ::ₘ {b⫠} by grind]
+      apply Proof.oplus₂
+      exact Proof.ax
+  case right =>
+    constructor
+    simp only [Proposition.dual]
+    apply Proof.with
+    · rw [show a'⫠ ::ₘ {a ⊕ b} = (a ⊕ b) ::ₘ {a'⫠} by grind]
+      apply Proof.oplus₁
+      apply h₂.rwConclusion (by grind)
+    · rw [show b⫠ ::ₘ {a ⊕ b} = (a ⊕ b) ::ₘ {b⫠} by grind]
+      apply Proof.oplus₂
+      exact Proof.ax
+
+@[local grind .]
+private lemma Proposition.equiv_oplus₂ {a b b' : Proposition Atom} (h : b ≡ b') :
+    a ⊕ b ≡ a ⊕ b' := by
+  obtain ⟨h₁, h₂⟩ := h
+  obtain h₁ := h₁.some
+  obtain h₂ := h₂.some
+  constructor
+  case left =>
+    constructor
+    simp only [Proposition.dual]
+    apply Proof.with
+    · rw [show a⫠ ::ₘ {a ⊕ b'} = (a ⊕ b') ::ₘ {a⫠} by grind]
+      apply Proof.oplus₁
+      exact Proof.ax
+    · rw [show b⫠ ::ₘ {a ⊕ b'} = (a ⊕ b') ::ₘ {b⫠} by grind]
+      apply Proof.oplus₂
+      apply h₁.rwConclusion (by grind)
+  case right =>
+    constructor
+    simp only [Proposition.dual]
+    apply Proof.with
+    · rw [show a⫠ ::ₘ {a ⊕ b} = (a ⊕ b) ::ₘ {a⫠} by grind]
+      apply Proof.oplus₁
+      exact Proof.ax
+    · rw [show b'⫠ ::ₘ {a ⊕ b} = (a ⊕ b) ::ₘ {b'⫠} by grind]
+      apply Proof.oplus₂
+      apply h₂.rwConclusion (by grind)
+
+@[local grind .]
+private lemma Proposition.equiv_with₁ {a a' b : Proposition Atom} (h : a ≡ a') :
+    a & b ≡ a' & b := by
+  obtain ⟨h₁, h₂⟩ := h
+  obtain h₁ := h₁.some
+  obtain h₂ := h₂.some
+  constructor
+  case left =>
+    constructor
+    simp only [Proposition.dual]
+    rw [show {a⫠ ⊕ b⫠, a' & b} = (a' & b) ::ₘ {a⫠ ⊕ b⫠} by grind]
+    apply Proof.with
+    · rw [show a' ::ₘ {a⫠ ⊕ b⫠} = (a⫠ ⊕ b⫠) ::ₘ {a'} by grind]
+      apply Proof.oplus₁
+      apply h₁.rwConclusion (by grind)
+    · rw [show b ::ₘ {a⫠ ⊕ b⫠} = (a⫠ ⊕ b⫠) ::ₘ {b} by grind]
+      apply Proof.oplus₂
+      exact Proof.ax'
+  case right =>
+    constructor
+    simp only [Proposition.dual]
+    rw [show {a'⫠ ⊕ b⫠, a & b} = (a & b) ::ₘ {a'⫠ ⊕ b⫠} by grind]
+    apply Proof.with
+    · rw [show a ::ₘ {a'⫠ ⊕ b⫠} = (a'⫠ ⊕ b⫠) ::ₘ {a} by grind]
+      apply Proof.oplus₁
+      apply h₂.rwConclusion (by grind)
+    · rw [show b ::ₘ {a'⫠ ⊕ b⫠} = (a'⫠ ⊕ b⫠) ::ₘ {b} by grind]
+      apply Proof.oplus₂
+      exact Proof.ax'
+
+@[local grind .]
+private lemma Proposition.equiv_with₂ {a b b' : Proposition Atom} (h : b ≡ b') :
+    a & b ≡ a & b' := by
+  obtain ⟨h₁, h₂⟩ := h
+  obtain h₁ := h₁.some
+  obtain h₂ := h₂.some
+  constructor
+  case left =>
+    constructor
+    simp only [Proposition.dual]
+    rw [show {a⫠ ⊕ b⫠, a & b'} = (a & b') ::ₘ {a⫠ ⊕ b⫠} by grind]
+    apply Proof.with
+    · rw [show a ::ₘ {a⫠ ⊕ b⫠} = (a⫠ ⊕ b⫠) ::ₘ {a} by grind]
+      apply Proof.oplus₁
+      exact Proof.ax'
+    · rw [show b' ::ₘ {a⫠ ⊕ b⫠} = (a⫠ ⊕ b⫠) ::ₘ {b'} by grind]
+      apply Proof.oplus₂
+      apply h₁.rwConclusion (by grind)
+  case right =>
+    constructor
+    simp only [Proposition.dual]
+    rw [show {a⫠ ⊕ b'⫠, a & b} = (a & b) ::ₘ {a⫠ ⊕ b'⫠} by grind]
+    apply Proof.with
+    · rw [show a ::ₘ {a⫠ ⊕ b'⫠} = (a⫠ ⊕ b'⫠) ::ₘ {a} by grind]
+      apply Proof.oplus₁
+      exact Proof.ax'
+    · rw [show b ::ₘ {a⫠ ⊕ b'⫠} = (a⫠ ⊕ b'⫠) ::ₘ {b} by grind]
+      apply Proof.oplus₂
+      apply h₂.rwConclusion (by grind)
+
+@[local grind .]
+private lemma Proposition.equiv_bang {a a' : Proposition Atom} (h : a ≡ a') :
+    !a ≡ !a' := by
+  obtain ⟨h₁, h₂⟩ := h
+  obtain h₁ := h₁.some
+  obtain h₂ := h₂.some
+  constructor
+  case left =>
+    constructor
+    simp only [Proposition.dual]
+    rw [show {ʔa⫠, !a'} = (!a') ::ₘ {ʔa⫠} by grind]
+    apply Proof.bang
+    · simp [allQuest, Multiset.fold]
+    · rw [show a' ::ₘ {ʔa⫠} = ʔa⫠ ::ₘ {a'} by grind]
+      apply Proof.quest
+      apply h₁.rwConclusion (by grind)
+  case right =>
+    constructor
+    simp only [Proposition.dual]
+    rw [show {ʔa'⫠, !a} = (!a) ::ₘ {ʔa'⫠} by grind]
+    apply Proof.bang
+    · simp [allQuest, Multiset.fold]
+    · rw [show a ::ₘ {ʔa'⫠} = ʔa'⫠ ::ₘ {a} by grind]
+      apply Proof.quest
+      apply h₂.rwConclusion (by grind)
+
+@[local grind .]
+private lemma Proposition.equiv_quest {a a' : Proposition Atom} (h : a ≡ a') :
+    ʔa ≡ ʔa' := by
+  obtain ⟨h₁, h₂⟩ := h
+  obtain h₁ := h₁.some
+  obtain h₂ := h₂.some
+  constructor
+  case left =>
+    constructor
+    simp only [Proposition.dual]
+    apply Proof.bang
+    · simp [allQuest, Multiset.fold]
+    · rw [show a⫠ ::ₘ {ʔa'} = ʔa' ::ₘ {a⫠} by grind]
+      apply Proof.quest
+      apply h₁.rwConclusion (by grind)
+  case right =>
+    constructor
+    simp only [Proposition.dual]
+    apply Proof.bang
+    · simp [allQuest, Multiset.fold]
+    · rw [show a'⫠ ::ₘ {ʔa} = ʔa ::ₘ {a'⫠} by grind]
+      apply Proof.quest
+      apply h₂.rwConclusion (by grind)
+
+instance : Congruence (Proposition Atom) Proposition.Equiv where
+  elim :
+      Covariant (Proposition.Context Atom) (Proposition Atom) (Proposition.Context.fill)
+      Proposition.Equiv := by
+    intro ctx a b hab
+    induction ctx <;> grind
+
+noncomputable instance : LogicalEquivalence (Proposition Atom) (Sequent Atom) Proof where
+  eqv := Proposition.Equiv
+  eqv_fill_valid {a b : Proposition Atom} (heqv : a.Equiv b)
+      (c : HasHContext.Context (Sequent Atom) (Proposition Atom))
+      (h : ⇓c<[a]) : ⇓c<[b] := by
+    apply subst_eqv_head (chooseEquiv heqv) h
+
 /-- Tensor is commutative. -/
 @[scoped grind =]
 def tensor_symm {a b : Proposition Atom} : a ⊗ b ≡⇓ b ⊗ a :=
@@ -387,8 +701,8 @@ def tensor_assoc {a b c : Proposition Atom} : a ⊗ (b ⊗ c) ≡⇓ (a ⊗ b) 
      show a⫠ ::ₘ b⫠ ::ₘ c⫠ ::ₘ {a ⊗ (b ⊗ c)} = ((a ⊗ (b ⊗ c)) ::ₘ {a⫠} + ({b⫠} + {c⫠})) by grind ▸
      (.tensor .ax <| .tensor .ax .ax)⟩
 
-instance {Γ : Sequent Atom} : Std.Symm (fun a b => Sequent.Provable ((a ⊗ b) ::ₘ Γ)) where
-  symm _ _ h := Sequent.Provable.fromProof (subst_eqv_head tensor_symm h.toProof)
+instance {Γ : Sequent Atom} : Std.Symm (fun a b => Derivable ((a ⊗ b) ::ₘ Γ)) where
+  symm _ _ h := Derivable.fromDerivation (subst_eqv_head tensor_symm (Derivable.toDerivation h))
 
 /-- ⊕ is idempotent. -/
 @[scoped grind =]
diff --git a/Cslib/Logics/LinearLogic/CLL/CutElimination.lean b/Cslib/Logics/LinearLogic/CLL/CutElimination.lean
index 7969a7d69..cc435d544 100644
--- a/Cslib/Logics/LinearLogic/CLL/CutElimination.lean
+++ b/Cslib/Logics/LinearLogic/CLL/CutElimination.lean
@@ -18,8 +18,10 @@ universe u
 
 variable {Atom : Type u}
 
+open Cslib.Logic.InferenceSystem
+
 /-- A proof is cut-free if it does not contain any applications of rule cut. -/
-def Proof.cutFree (p : ⇓Γ) : Bool :=
+def Proof.cutFree {Γ : Sequent Atom} (p : ⇓Γ) : Bool :=
   match p with
   | ax => true
   | one => true
diff --git a/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean b/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean
index ab891c49d..de4cfdb95 100644
--- a/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean
+++ b/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean
@@ -25,10 +25,12 @@ attribute [local grind =] Multiset.add_comm
 attribute [local grind =] Multiset.add_assoc
 attribute [local grind =] Multiset.insert_eq_cons
 
+open Cslib.Logic.InferenceSystem
+
 /-- The η-expansion of a proposition `a` is a `Proof` of `{a, a⫠}` that applies the axiom
 only to atomic propositions. -/
 @[scoped grind =]
-def Proposition.expand (a : Proposition Atom) : ⇓{a, a⫠} :=
+def Proposition.expand (a : Proposition Atom) : ⇓({a, a⫠} : Sequent Atom):=
   match a with
   | atom x
     | atomDual x => Proof.ax
@@ -80,7 +82,7 @@ decreasing_by
 
 /-- A `Proof` has only atomic axioms if all its instances of the axiom treat atomic propositions. -/
 @[scoped grind =]
-def Proof.onlyAtomicAxioms (p : ⇓Γ) : Bool :=
+def Proof.onlyAtomicAxioms {Γ : Sequent Atom} (p : ⇓Γ) : Bool :=
   match p with
   | @ax _ a => (a matches Proposition.atom _) || (a matches Proposition.atomDual _)
   | cut p q => p.onlyAtomicAxioms && q.onlyAtomicAxioms
@@ -98,8 +100,9 @@ def Proof.onlyAtomicAxioms (p : ⇓Γ) : Bool :=
   | bang _ p => p.onlyAtomicAxioms
 
 /-- `Proof.onlyAtomicAxioms` is preserved by `Proof.rwConclusion`. -/
-theorem Proof.onlyAtomicAxioms_rwConclusion {heq : Γ = Δ} {p : ⇓Γ} (h : p.onlyAtomicAxioms) :
-  (p.rwConclusion heq).onlyAtomicAxioms := by grind
+theorem Proof.onlyAtomicAxioms_rwConclusion {Γ Δ : Sequent Atom} {heq : Γ = Δ} {p : ⇓Γ}
+    (h : p.onlyAtomicAxioms) :
+  (rwConclusion heq p).onlyAtomicAxioms := by grind
 
 open Proposition Proof in
 @[local grind →]
diff --git a/CslibTests/CLL.lean b/CslibTests/CLL.lean
index 4864a9299..a4d81a42f 100644
--- a/CslibTests/CLL.lean
+++ b/CslibTests/CLL.lean
@@ -71,6 +71,8 @@ example : (a⫠ = b⫠) ↔ (a = b) := Proposition.dual_inj a b
 
 /-! ## Basic proof tests -/
 
+open scoped Cslib.Logic.InferenceSystem
+
 -- Axiom: ⊢ a, a⫠
 example : ⇓({a, a⫠} : Sequent Nat) := Proof.ax
 example : ⇓({a⫠, a} : Sequent Nat) := Proof.ax'