diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
index fb6e3bc7ddd6efd5f086afc83afd809530d3a3c1..cb97199b9c76b8f7361b6ade3c854d3369a3340b 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
@@ -48,7 +48,7 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
 
   case object Implies extends ConstantConnectorLabel("⇒", 2)
 
-  case object Iff extends ConstantConnectorLabel("↔", 2)
+  case object Iff extends ConstantConnectorLabel("⇔", 2)
 
   case object And extends ConstantConnectorLabel("∧", -1)
 
diff --git a/lisa-utils/src/main/scala/lisa/utils/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
index 1cb6546d4946d67c7b51f9b30f89eca1d82bf7fe..b4d179bbc9af893694293238a7a394c5893e7985 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Parser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
@@ -161,8 +161,8 @@ object Parser {
       elem('=') |> { _ => EqualityToken },
       elem('∧') | word("/\\") |> { _ => AndToken },
       elem('∨') | word("\\/") |> { _ => OrToken },
-      elem('⇒') | word("=>") | word("==>") |> { _ => ImpliesToken },
-      elem('↔') | word("<=>") | word("<==>") |> { _ => IffToken },
+      word(Implies.id) | word("=>") | word("==>") | elem('→') |> { _ => ImpliesToken },
+      word(Iff.id) | word("<=>") | word("<==>") | elem('⟷') | elem('↔') |> { _ => IffToken },
       elem('⊤') | elem('T') | word("True") | word("true") |> { _ => TrueToken },
       elem('⊥') | elem('F') | word("False") | word("false") |> { _ => FalseToken },
       elem('¬') | elem('!') |> { _ => NegationToken },
diff --git a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
index 8930b571eae0e8aaca64ca51164be202c93e0511..f945193d6a70fe68cd936e7273607741fdf034cc 100644
--- a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
@@ -74,6 +74,7 @@ class ParserTest extends AnyFunSuite with TestUtils {
     assert(Parser.parseFormula("a ∨ b") == ConnectorFormula(Or, Seq(a, b)))
     assert(Parser.parseFormula("a ⇒ b") == ConnectorFormula(Implies, Seq(a, b)))
     assert(Parser.parseFormula("a ↔ b") == ConnectorFormula(Iff, Seq(a, b)))
+    assert(Parser.parseFormula("a ⇔ b") == ConnectorFormula(Iff, Seq(a, b)))
   }
 
   test("ascii connectors") {
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index e8c2a63c90a58f899a4306ff19a9a69046386a8b..a15b86b89d0ece8d3eb5ae20a11db66165e9dd4e 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -90,7 +90,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
     assert(Parser.printFormula(ConnectorFormula(And, Seq(a, b))) == "a ∧ b")
     assert(Parser.printFormula(ConnectorFormula(Or, Seq(a, b))) == "a ∨ b")
     assert(Parser.printFormula(ConnectorFormula(Implies, Seq(a, b))) == "a ⇒ b")
-    assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, b))) == "a ↔ b")
+    assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, b))) == "a ⇔ b")
   }
 
   test("connector associativity") {
@@ -129,13 +129,13 @@ class PrinterTest extends AnyFunSuite with TestUtils {
     assert(Parser.printFormula(ConnectorFormula(Implies, Seq(a, ConnectorFormula(Or, Seq(b, c))))) == "a ⇒ b ∨ c")
 
     // (a ∧ b) <=> c
-    assert(Parser.printFormula(ConnectorFormula(Iff, Seq(ConnectorFormula(And, Seq(a, b)), c))) == "a ∧ b ↔ c")
+    assert(Parser.printFormula(ConnectorFormula(Iff, Seq(ConnectorFormula(And, Seq(a, b)), c))) == "a ∧ b ⇔ c")
     // a <=> (b ∧ c)
-    assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, ConnectorFormula(And, Seq(b, c))))) == "a ↔ b ∧ c")
+    assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, ConnectorFormula(And, Seq(b, c))))) == "a ⇔ b ∧ c")
     // (a ∨ b) <=> c
-    assert(Parser.printFormula(ConnectorFormula(Iff, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "a ∨ b ↔ c")
+    assert(Parser.printFormula(ConnectorFormula(Iff, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "a ∨ b ⇔ c")
     // a <=> (b ∨ c)
-    assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, ConnectorFormula(Or, Seq(b, c))))) == "a ↔ b ∨ c")
+    assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, ConnectorFormula(Or, Seq(b, c))))) == "a ⇔ b ∨ c")
   }
 
   test("connector parentheses") {
@@ -228,7 +228,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
           Set(BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(x === x1, sPhi1(x))))),
           Set((z === sf1(x1)) ==> exists(x, (z === sf1(x)) /\ sPhi1(x)))
         )
-      ) == "∀ ?x. ?x = ?x1 ↔ ?phi(?x) ⊢ ?z = ?f(?x1) ⇒ (∃ ?x. ?z = ?f(?x) ∧ ?phi(?x))"
+      ) == "∀ ?x. ?x = ?x1 ⇔ ?phi(?x) ⊢ ?z = ?f(?x1) ⇒ (∃ ?x. ?z = ?f(?x) ∧ ?phi(?x))"
     )
     assert(
       Parser.printSequent(
@@ -236,7 +236,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
           z1,
           forall(z, (z === z1) <=> exists(x, (z === sf1(x)) /\ sPhi1(x)))
         )
-      ) == "∃ ?x1. ∀ ?x. ?x = ?x1 ↔ ?phi(?x) ⊢ ∃ ?z1. ∀ ?z. ?z = ?z1 ↔ (∃ ?x. ?z = ?f(?x) ∧ ?phi(?x))"
+      ) == "∃ ?x1. ∀ ?x. ?x = ?x1 ⇔ ?phi(?x) ⊢ ∃ ?z1. ∀ ?z. ?z = ?z1 ⇔ (∃ ?x. ?z = ?f(?x) ∧ ?phi(?x))"
     )
     assert(Parser.printSequent((() |- (x === x) \/ (x === y))) == "⊢ ?x = ?x ∨ ?x = ?y")
     assert(
@@ -245,7 +245,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
           (x === x) \/ (x === y),
           ((x === x) \/ (x === y)) <=> ((x === xPrime) \/ (x === yPrime))
         ) |- (x === xPrime) \/ (x === yPrime)
-      ) == "?x = ?x ∨ ?x = ?y; ?x = ?x ∨ ?x = ?y ↔ ?x = ?x' ∨ ?x = ?y' ⊢ ?x = ?x' ∨ ?x = ?y'"
+      ) == "?x = ?x ∨ ?x = ?y; ?x = ?x ∨ ?x = ?y ⇔ ?x = ?x' ∨ ?x = ?y' ⊢ ?x = ?x' ∨ ?x = ?y'"
     )
   }
 }