diff --git a/lisa-sets2/src/main/scala/lisa/automation/Congruence.scala b/lisa-sets2/src/main/scala/lisa/automation/Congruence.scala
index 905bad78..75784aa2 100644
--- a/lisa-sets2/src/main/scala/lisa/automation/Congruence.scala
+++ b/lisa-sets2/src/main/scala/lisa/automation/Congruence.scala
@@ -37,8 +37,8 @@ object Congruence  extends ProofTactic with ProofSequentTactic {
     egraph.addAll(bot.right)
     
     bot.left.foreach{
-      case `===` #@ l #@ r => egraph.merge(l, r)
-      case `<=>` #@ l #@ r => egraph.merge(l, r)
+      case === #@ l #@ r => egraph.merge(l, r)
+      case <=> #@ l #@ r => egraph.merge(l, r)
       case _ => ()
     }
 
@@ -66,10 +66,10 @@ object Congruence  extends ProofTactic with ProofSequentTactic {
         case _  => false
       } || {
       lf match
-        case neg  #@ (`===` #@ a #@ b) if egraph.idEq(a, b) => 
+        case neg  #@ (=== #@ a #@ b) if egraph.idEq(a, b) => 
           have(egraph.proveExpr(a, b, bot))
           true
-        case neg  #@  (`<=>` #@ a #@ b) if egraph.idEq(a, b) => 
+        case neg  #@  (<=> #@ a #@ b) if egraph.idEq(a, b) => 
           have(egraph.proveExpr(a, b, bot))
           true
         case _ => false
@@ -88,10 +88,10 @@ object Congruence  extends ProofTactic with ProofSequentTactic {
         case _  => false
       } || {
       rf match
-        case (`===` #@ a #@ b) if egraph.idEq(a, b) => 
+        case (=== #@ a #@ b) if egraph.idEq(a, b) => 
           have(egraph.proveExpr(a, b, bot))
           true
-        case (`<=>` #@ a #@ b) if egraph.idEq(a, b) =>
+        case (<=> #@ a #@ b) if egraph.idEq(a, b) =>
           have(egraph.proveExpr(a, b, bot))
           true
         case _ => false
diff --git a/lisa-sets2/src/main/scala/lisa/automation/Substitution.scala b/lisa-sets2/src/main/scala/lisa/automation/Substitution.scala
index fa28cbed..a1f6f066 100644
--- a/lisa-sets2/src/main/scala/lisa/automation/Substitution.scala
+++ b/lisa-sets2/src/main/scala/lisa/automation/Substitution.scala
@@ -28,8 +28,8 @@ object Substitution:
     (rule: proof.Fact | F.Formula): RewriteRule =
       rule match
         case f: Formula @unchecked => (f: @unchecked) match
-          case `===` #@ (l: Term) #@ (r: Term) => TermRewriteRule(l, r)
-          case `<=>` #@ (l: Formula) #@ (r: Formula) => FormulaRewriteRule(l, r)
+          case === #@ (l: Term) #@ (r: Term) => TermRewriteRule(l, r)
+          case <=> #@ (l: Formula) #@ (r: Formula) => FormulaRewriteRule(l, r)
         case f: proof.Fact @unchecked => extractRule(proof.getSequent(f).right.head)
 
   /**
@@ -61,8 +61,8 @@ object Substitution:
     (rule: (proof.Fact | F.Formula)): Boolean =
       rule match
         // as formula
-        case f: Formula @ unchecked => f match
-          case ===(l, r) => true
+        case f: Formula @unchecked => f match
+          case === #@ l #@ r => true
           case <=> #@ l #@ r => true
           case _ => false
         // as a justification