diff --git a/Cslib.lean b/Cslib.lean
index 43c374ae7..4f558680b 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -77,6 +77,7 @@ 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.Logic.Operators
 public import Cslib.Foundations.Relation.Attr
 public import Cslib.Foundations.Relation.Confluence
 public import Cslib.Foundations.Relation.Defs
diff --git a/Cslib/Foundations/Logic/LogicalEquivalence.lean b/Cslib/Foundations/Logic/LogicalEquivalence.lean
index 7f6c0d332..f4dbc06d9 100644
--- a/Cslib/Foundations/Logic/LogicalEquivalence.lean
+++ b/Cslib/Foundations/Logic/LogicalEquivalence.lean
@@ -8,6 +8,7 @@ module
 
 public import Cslib.Foundations.Syntax.Context
 public import Cslib.Foundations.Syntax.Congruence
+public import Cslib.Foundations.Logic.InferenceSystem
 
 /-! Typeclass and notation for logical equivalence. -/
 
@@ -15,21 +16,33 @@ public import Cslib.Foundations.Syntax.Congruence
 
 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
+class LogicalEquivalence S
     (Proposition : Type u) [HasContext Proposition]
     (Judgement : Type v) [HasHContext Judgement Proposition]
-    (Valid : Judgement → Sort w) where
-  /-- The logical equivalence relation. -/
+    [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]
   /-- Validity is preserved for any judgemental context. -/
   eqvFillValid (heqv : eqv a b) (c : HasHContext.Context Judgement Proposition)
-    (h : Valid (c<[a])) : Valid (c<[b])
+    (h : S⇓(c<[a])) : S⇓(c<[b])
 
 @[inherit_doc]
-scoped infix:29 " ≡ " => LogicalEquivalence.eqv
+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/Logic/Operators.lean b/Cslib/Foundations/Logic/Operators.lean
new file mode 100644
index 000000000..ab6a463b7
--- /dev/null
+++ b/Cslib/Foundations/Logic/Operators.lean
@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi, Thomas Waring
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # Logical operators
+
+This module contains typeclasses and associated notation for common logical operators: propositional
+connectives (like `∧` and `→`), modalities (like `◇`, plain and indexed), linear connectives (like
+`⊗`), etc.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+section Propositional
+
+/-! ## Propositional connectives -/
+
+/-- The type `α` has an and connective (`∧`). -/
+class HasAnd (α : Type*) where
+  /-- `a ∧ b` is the conjunction of `a` and `b`. -/
+  and (a b : α) : α
+
+@[inherit_doc] scoped infixr:36 " ∧ " => HasAnd.and
+
+/-- The type `α` has an or connective (`∨`). -/
+class HasOr (α : Type*) where
+  /-- `a ∨ b` is the disjunction of `a` and `b`. -/
+  or (a b : α) : α
+
+@[inherit_doc] scoped infixr:30 " ∨ " => HasOr.or
+
+/-- The type `α` has an implication connective (`→`). -/
+class HasImp (α : Type*) where
+  /-- `a → b` denotes `a` implies `b`. -/
+  imp (a b : α) : α
+
+@[inherit_doc] scoped infixr:25 " → " => HasImp.imp
+
+/-- The type `α` has a bi-implication connective (`↔`). -/
+class HasIff (α : Type*) where
+  /-- `a ↔ b` denotes `a` implies `b` and vice-versa. -/
+  iff (a b : α) : α
+
+@[inherit_doc] scoped infixr:20 " ↔ " => HasIff.iff
+
+/-- The type `α` has a negation connective (`¬`). -/
+class HasNot (α : Type*) where
+  /-- `¬a` is the negation of `a`. -/
+  not (a : α) : α
+
+@[inherit_doc] scoped notation:max "¬" p:40 => HasNot.not p
+
+end Propositional
+
+section Modal
+
+/-! ## Basic modalities -/
+
+/-- The type `α` has a box modality (`□`). -/
+class HasBox (α : Type*) where
+  /-- `a` is valid in all immediately reachable states. -/
+  box (a : α) : α
+
+@[inherit_doc] scoped prefix:40 "□" => HasBox.box
+
+/-- The type `α` has a diamond modality (`◇`). -/
+class HasDiamond (α : Type*) where
+  /-- `a` is valid in a reachable state. -/
+  diamond (a : α) : α
+
+@[inherit_doc] scoped prefix:40 "◇" => HasDiamond.diamond
+
+end Modal
+
+/-
+section Dynamic
+
+/-! ## Dynamic modalities  -/
+
+/-- The type `α` has a dynamic box modality with action type `β` (`[a]φ`). -/
+class HasDynamicBox (α β : Type*) where
+  /-- `b` is necessarily valid after `a`. -/
+  dynBox (a : β) (b : α) : α
+
+@[inherit_doc] scoped notation "[" a "]" φ => HasDynamicBox.dynBox a φ
+
+/-- The type `α` has a dynamic diamond modality with action type `β` (`[a]φ`). -/
+class HasDynamicDiamond (α β : Type*) where
+  /-- `b` is possibly valid after `a`. -/
+  dynDiamond (a : β) (b : α) : α
+
+@[inherit_doc] scoped notation "⟨" a "⟩" φ => HasDynamicDiamond.dynDiamond a φ
+
+end Dynamic
+-/
+
+section Linear
+
+/-! ## Linear connectives -/
+
+/-- The type `α` has a tensor connective (⊗). -/
+class HasTensor (α : Type*) where
+  /-- `a ⊗ b` is the multiplicative conjunction of `a` and `b`. -/
+  tensor (a b : α) : α
+
+@[inherit_doc] scoped infixr:35 " ⊗ " => HasTensor.tensor
+
+end Linear
+
+end Cslib.Logic
diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean
index 5bad96e46..2e0c8005a 100644
--- a/Cslib/Logics/HML/LogicalEquivalence.lean
+++ b/Cslib/Logics/HML/LogicalEquivalence.lean
@@ -81,6 +81,8 @@ structure Satisfies.Judgement (State : Type u) (Label : Type v) where
 /-- `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
 
@@ -102,8 +104,8 @@ 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
+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))
diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean
index c331ae2ae..ce8db29a4 100644
--- a/Cslib/Logics/LinearLogic/CLL/Basic.lean
+++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean
@@ -650,7 +650,7 @@ instance : Congruence (Proposition Atom) Proposition.Equiv where
     intro ctx a b hab
     induction ctx <;> grind [= Context.fill]
 
-noncomputable instance : LogicalEquivalence (Proposition Atom) (Sequent Atom) Proof where
+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))
diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index fda217a1c..cefa5bece 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -6,7 +6,7 @@ Authors: Fabrizio Montesi, Marianna Girlando
 
 module
 
-public import Cslib.Init
+public import Cslib.Foundations.Logic.Operators
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Mathlib.Data.Set.Basic
 public import Mathlib.Order.Defs.Unbundled
@@ -47,29 +47,51 @@ inductive Proposition (Atom : Type u) : Type u where
   /-- Possibility. -/
   | diamond (φ : Proposition Atom)
 
-@[inherit_doc] scoped prefix:40 "¬" => Proposition.not
-@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and
-@[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond
+instance : HasNot (Proposition Atom) := {not := Proposition.not}
+instance : HasAnd (Proposition Atom) := {and := Proposition.and}
+instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond}
+
+@[scoped grind =]
+lemma Proposition.not_def (φ : Proposition Atom) : φ.not = ¬φ := rfl
+
+@[scoped grind =]
+lemma Proposition.and_def (φ₁ φ₂ : Proposition Atom) : φ₁.and φ₂ = (φ₁ ∧ φ₂) := rfl
+
+@[scoped grind =]
+lemma Proposition.diamond_def (φ : Proposition Atom) : φ.diamond = (◇φ) := rfl
 
 /-- Disjunction. -/
 def Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬(¬φ₁ ∧ ¬φ₂)
 
-@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or
+instance : HasOr (Proposition Atom) := {or := Proposition.or}
+
+@[scoped grind =]
+lemma Proposition.or_def (φ₁ φ₂ : Proposition Atom) : φ₁.or φ₂ = (φ₁ ∨ φ₂) := rfl
 
 /-- Implication. -/
-def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂
+def Proposition.imp (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂
+
+instance : HasImp (Proposition Atom) := {imp := Proposition.imp}
 
-@[inherit_doc] scoped infix:30 " → " => Proposition.impl
+@[scoped grind =]
+lemma Proposition.imp_def (φ₁ φ₂ : Proposition Atom) : φ₁.imp φ₂ = (φ₁ → φ₂) := rfl
 
 /-- Bi-implication. -/
 def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁)
 
-@[inherit_doc] scoped infix:30 " ↔ " => Proposition.iff
+instance : HasIff (Proposition Atom) := {iff := Proposition.iff}
+
+@[scoped grind =]
+lemma Proposition.iff_def (φ₁ φ₂ : Proposition Atom) :
+    φ₁.iff φ₂ = (φ₁ ↔ φ₂) := rfl
 
 /-- Necessity. -/
 def Proposition.box (φ : Proposition Atom) : Proposition Atom := ¬◇¬φ
 
-@[inherit_doc] scoped prefix:40 "□" => Proposition.box
+instance : HasBox (Proposition Atom) := {box := Proposition.box}
+
+@[scoped grind =]
+lemma Proposition.box_def (φ : Proposition Atom) : φ.box = (□φ) := rfl
 
 /-- Satisfaction relation. `Satisfies m w φ` means that, in the model `m`, the world `w` satisfies
 the proposition `φ`. -/
@@ -107,8 +129,15 @@ theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom
 
 /-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/
 @[scoped grind =]
-theorem not_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by
-  induction φ generalizing w <;> grind
+theorem Satisfies.not_iff_not : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by rfl
+
+@[scoped grind =]
+theorem Satisfies.and_iff_and {m : Model World Atom} :
+    ⇓Modal[m,w ⊨ φ₁ ∧ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∧ ⇓Modal[m,w ⊨ φ₂] := by rfl
+
+@[scoped grind =]
+theorem Satisfies.diamond_iff_exists {m : Model World Atom} :
+    ⇓Modal[m,w ⊨ ◇φ] ↔ ∃ w', m.r w w' ∧ ⇓Modal[m,w' ⊨ φ] := by rfl
 
 /-- Characterisation of the `∨` connective.
 
@@ -116,7 +145,8 @@ Disjunction is defined in terms of the more primitive connectives given in `Prop
 This result proves that the definition is correct. -/
 @[scoped grind =]
 theorem Satisfies.or_iff_or {m : Model World Atom} :
-    ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by grind [Proposition.or]
+    ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by
+  grind [=_ Proposition.or_def, Proposition.or]
 
 /-- Characterisation of the `→` connective.
 
@@ -124,8 +154,9 @@ Implication is defined in terms of the more primitive connectives given in `Prop
 This result proves that the definition is correct.
 -/
 @[scoped grind =]
-theorem Satisfies.impl_iff_impl {m : Model World Atom} :
-    ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by grind [Proposition.impl]
+theorem Satisfies.imp_iff_imp {m : Model World Atom} :
+    ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by
+  grind [=_ Proposition.imp_def, Proposition.imp]
 
 /-- Characterisation of the `↔` connective.
 
@@ -134,7 +165,7 @@ This result proves that the definition is correct. -/
 @[scoped grind =]
 theorem Satisfies.iff_iff_iff {m : Model World Atom} :
     ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by
-  simp only [Proposition.iff]
+  simp only [HasIff.iff, Proposition.iff]
   grind [= derivation_def]
 
 /-- Characterisation of the `□` modality.
@@ -143,7 +174,8 @@ Necessity is defined in terms of the more primitive connectives given in `Propos
 This result proves that the definition is correct. -/
 @[scoped grind =]
 theorem Satisfies.box_iff_forall {m : Model World Atom} :
-    ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by grind [Proposition.box]
+    ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by
+  grind [=_ Proposition.box_def, Proposition.box]
 
 /-- The theory of a world in a model is the set of all propositions that it satifies. -/
 abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) :=
@@ -162,7 +194,7 @@ theorem satisfies_theory (h : Satisfies m w φ) : φ ∈ theory m w := by grind
 
 /-- If two worlds are not theory equivalent, there exists a distinguishing proposition. -/
 lemma not_theoryEq_satisfies (h : ¬TheoryEq m w₁ w₂) :
-    ∃ φ, (⇓Modal[m,w₁ ⊨ φ] ∧ ¬⇓Modal[m,w₂ ⊨ φ]) := by grind [=_ not_satisfies]
+    ∃ φ, (⇓Modal[m,w₁ ⊨ φ] ∧ ¬⇓Modal[m,w₂ ⊨ φ]) := by grind [=_ Satisfies.not_iff_not]
 
 /-- If two worlds are theory equivalent and the former satisfies a proposition, the latter does as
 well. -/
@@ -174,11 +206,13 @@ theorem theoryEq_satisfies {m : Model World Atom} (h : TheoryEq m w₁ w₂)
 /-- The K axiom, valid for all models. -/
 theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)] := by grind
 
-set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- The dual axiom, valid for all models. -/
 theorem Satisfies.dual : ⇓Modal[m,w ⊨ ◇φ ↔ ¬□¬φ] := by
-  grind only [Satisfies.iff_iff_iff.mpr, → satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl,
-    =_ derivation_def, = not_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true]
+  constructor
+  · grind
+  · grind
+    --  only [→ satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl, = derivation_def,
+    -- = not_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true]
 
 /-- The T axiom, valid for all reflexive models. -/
 theorem Satisfies.t {m : Model World Atom} [instRefl : Std.Refl m.r] {w : World}
@@ -211,13 +245,13 @@ theorem Satisfies.b_symm {World Atom} {r : World → World → Prop} [Nonempty A
     have a := Classical.arbitrary Atom
     let v₁ := fun (w' : World) (a : Atom) => w' = w₁
     let h₁ := h (v := v₁) (w := w₁) (φ := .atom a)
-    simp [impl_iff_impl] at h₁
+    simp [imp_iff_imp] at h₁
     grind
 
 /-- The 4 axiom, valid for all transitive models. -/
 theorem Satisfies.four {m : Model World Atom} [IsTrans World m.r] {w : World}
     (φ : Proposition Atom) : ⇓Modal[m,w ⊨ ◇◇φ → ◇φ] := by
-  simp only [impl_iff_impl]
+  simp only [imp_iff_imp]
   intro h
   rcases h with ⟨w', h₁, w'', h₂, hs⟩
   exact ⟨w'', IsTrans.trans _ _ _ h₁ h₂, hs⟩
diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean
index b74e8f3f1..4b3415b33 100644
--- a/Cslib/Logics/Modal/Denotation.lean
+++ b/Cslib/Logics/Modal/Denotation.lean
@@ -18,7 +18,7 @@ A denotational semantics for modal logic, inspired by the one for Hennessy-Milne
 
 namespace Cslib.Logic.Modal
 
-open scoped Proposition InferenceSystem
+open scoped Proposition InferenceSystem Satisfies
 
 /-- Denotation of a proposition. -/
 @[simp, scoped grind =]
diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index 0fc089e4e..0f34ad0e5 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -122,8 +122,8 @@ lemma Satisfies.Context.fill_def {c : Satisfies.Context World Atom} :
 open scoped Satisfies.Context
 
 /-- Logical equivalence for Modal Logic K. That is, no assumptions on models are made. -/
-instance : LogicalEquivalence
-    (Proposition Atom) (Judgement World Atom) Satisfies.Bundled where
+instance : HasLogicalEquivalence
+    (Proposition Atom) (Judgement World Atom) where
   eqv := Proposition.Equiv Set.univ
   eqvFillValid heqv c h := by
     specialize heqv c.m
diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean
index e9c603d91..cea4c2362 100644
--- a/Cslib/Logics/Propositional/Defs.lean
+++ b/Cslib/Logics/Propositional/Defs.lean
@@ -6,6 +6,7 @@ Authors: Thomas Waring
 
 module
 
+public import Cslib.Foundations.Logic.Operators
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Mathlib.Data.FunLike.Basic
 public import Mathlib.Data.Set.Image
@@ -30,8 +31,10 @@ theory.
 
 ## Notation
 
-We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum,
-conjunction, disjunction, implication and negation.
+We instantiate the notation classes `HasAnd`, `HasOr`, `HasImpl` and `HasNot` for `Proposition Atom`
+to give access to, respectively, the notations `∧, ∨, →` and `¬` for propositional connectives.
+In the case that `Atom` has a bottom element (respectively, is inhabited) we give instances
+`HasBot (Proposition Atom)` and (respectively, `HasTop (Proposition Atom)`).
 -/
 
 @[expose] public section
@@ -51,26 +54,30 @@ inductive Proposition (Atom : Type u) : Type u where
   /-- Disjunction -/
   | or (a b : Proposition Atom)
   /-- Implication -/
-  | impl (a b : Proposition Atom)
+  | imp (a b : Proposition Atom)
 deriving DecidableEq, BEq
 
 instance instBotProposition [Bot Atom] : Bot (Proposition Atom) := ⟨.atom ⊥⟩
 instance instInhabitedOfBot [Bot Atom] : Inhabited Atom := ⟨⊥⟩
 
 /-- We view negation as a defined connective ~A := A → ⊥ -/
-abbrev Proposition.neg [Bot Atom] : Proposition Atom → Proposition Atom := (Proposition.impl · ⊥)
+abbrev Proposition.neg [Bot Atom] : Proposition Atom → Proposition Atom := (Proposition.imp · ⊥)
 
 /-- A fixed choice of a derivable proposition (of course any two are equivalent). -/
-abbrev Proposition.top [Inhabited Atom] : Proposition Atom := impl (.atom default) (.atom default)
+abbrev Proposition.top [Inhabited Atom] : Proposition Atom := imp (.atom default) (.atom default)
 
 instance instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top⟩
 
-example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl
+example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.imp ⊥ ⊥ := rfl
 
-@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and
-@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or
-@[inherit_doc] scoped infix:30 " → " => Proposition.impl
-@[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg
+instance : HasAnd (Proposition Atom) := {and := Proposition.and}
+instance : HasOr (Proposition Atom) := {or := Proposition.or}
+instance : HasImp (Proposition Atom) := {imp := Proposition.imp}
+instance [Bot Atom] : HasNot (Proposition Atom) := {not := Proposition.neg}
+
+omit [DecidableEq Atom] in
+@[grind =]
+lemma not_eq [Bot Atom] (A : Proposition Atom) : (A → ⊥) = ¬ A := rfl
 
 /-- Substitute each atom in a proposition for a proposition, possibly changing the atomic
 language. -/
@@ -79,7 +86,7 @@ def Proposition.subst {Atom Atom' : Type u} (f : Atom → Proposition Atom') :
   | atom x => f x
   | and A B => (A.subst f) ∧ (B.subst f)
   | or A B => (A.subst f) ∨ (B.subst f)
-  | impl A B => (A.subst f) → (B.subst f)
+  | imp A B => (A.subst f) → (B.subst f)
 
 -- This is probably a lawful monad, but that doesn't seem to be important.
 instance : Monad Proposition where