diff --git a/src/test/scala/lisa/automation/ProofTests.scala b/src/test/scala/lisa/automation/ProofTests.scala
index b140c082e791338925c6c1d8b861e174c8334f59..4bc569ba16591ac4b3e6ac17bb15572150c37086 100644
--- a/src/test/scala/lisa/automation/ProofTests.scala
+++ b/src/test/scala/lisa/automation/ProofTests.scala
@@ -17,98 +17,158 @@ class ProofTests extends AnyFunSuite {
   val (s, t, u) = (SchematicTermLabel[0]("s"), SchematicTermLabel[0]("t"), SchematicTermLabel[0]("u"))
   val (x, y) = (VariableLabel("x"), VariableLabel("y"))
 
-  private def checkProofs(proofs: Proof*): Unit = {
+  private def checkProof(proof: Proof): Unit = {
     val emptyEnvironment: ProofEnvironment = newEmptyEnvironment()
-    proofs.foreach { proof =>
-      val result = evaluateProof(proof)(emptyEnvironment).map(reconstructSCProof)
-      assert(result.nonEmpty)
-      val scProof = result.get._1
-      val judgement = SCProofChecker.checkSCProof(scProof)
-      println(Printer.prettySCProof(judgement))
-      println()
-      assert(judgement.isValid)
-      assert(scProof.imports.isEmpty)
-      assert(lisa.kernel.proof.SequentCalculus.isSameSequent(scProof.conclusion, proof.initialState.goals.head))
-    }
+    val result = evaluateProof(proof)(emptyEnvironment).map(reconstructSCProof)
+    assert(result.nonEmpty, s"kernel proof was empty for $proof")
+    val scProof = result.get._1
+    val judgement = SCProofChecker.checkSCProof(scProof)
+    assert(judgement.isValid, Printer.prettySCProof(judgement))
+    assert(scProof.imports.isEmpty, s"proof unexpectedly uses imports: ${Printer.prettySCProof(judgement)}")
+    assert(
+      lisa.kernel.proof.SequentCalculus.isSameSequent(scProof.conclusion, proof.initialState.goals.head),
+      s"proof does not prove ${Printer.prettySequent(proof.initialState.goals.head)}:\nPrinter.prettySCProof(judgement)"
+    )
   }
 
-  test("introduction rules") {
-    checkProofs(
+  test("hypothesis") {
+    checkProof(
       Proof(
         (a, b /\ c) |- (b /\ c, b)
       )(
         RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
-      ),
+      )
+    )
+
+  }
+
+  test("left and") {
+    checkProof(
       Proof(
         (a /\ b) |- a
       )(
         RuleIntroductionLeftAnd(),
         RuleHypothesis(RuleParameters().withIndices(0)(0)(0))
-      ),
+      )
+    )
+  }
+
+  test("right and") {
+    checkProof(
       Proof(
         (a, b) |- (a /\ b)
       )(
         RuleIntroductionRightAnd(RuleParameters().withIndices(0)()(0)),
         RuleHypothesis(RuleParameters().withIndices(0)(0)(0)),
         RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
-      ),
+      )
+    )
+  }
+
+  test("left or") {
+    checkProof(
       Proof(
         (a \/ b) |- (a, b)
       )(
         RuleIntroductionLeftOr(RuleParameters().withIndices(0)(0)()),
         RuleHypothesis(RuleParameters().withIndices(0)(0)(0)),
         RuleHypothesis(RuleParameters().withIndices(0)(0)(1))
-      ),
+      )
+    )
+  }
+
+  test("right or") {
+    checkProof(
       Proof(
         a |- (a \/ b)
       )(
         RuleIntroductionRightOr(RuleParameters().withIndices(0)()(0)),
         RuleHypothesis(RuleParameters().withIndices(0)(0)(0))
-      ),
+      )
+    )
+  }
+
+  test("left implies") {
+    checkProof(
       Proof(
         (a ==> b, a) |- b
       )(
         RuleIntroductionLeftImplies(RuleParameters().withIndices(0)(0)()),
         RuleHypothesis(RuleParameters().withIndices(0)(0)(1)),
         RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
-      ),
+      )
+    )
+  }
+
+  test("right implies") {
+    checkProof(
       Proof(
         () |- (a ==> a)
       )(
         RuleIntroductionRightImplies(RuleParameters().withIndices(0)()(0)),
         RuleHypothesis(RuleParameters().withIndices(0)(0)(0))
-      ),
+      )
+    )
+  }
+
+  test("left iff") {
+    checkProof(
       Proof(
         (a <=> b) |- (b ==> a)
       )(
         RuleIntroductionLeftIff(RuleParameters().withIndices(0)(0)()),
         RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
-      ),
+      )
+    )
+  }
+
+  test("right iff") {
+    checkProof(
       Proof(
         (a ==> b, b ==> a) |- (a <=> b)
       )(
         RuleIntroductionRightIff(RuleParameters().withIndices(0)()(0)),
         RuleHypothesis(RuleParameters().withIndices(0)(0)(0)),
         RuleHypothesis(RuleParameters().withIndices(0)(1)(0))
-      ),
+      )
+    )
+  }
+
+  test("left not") {
+    checkProof(
       Proof(
         (a, !a) |- b
       )(
         RuleIntroductionLeftNot(RuleParameters().withIndices(0)(1)()),
         RuleHypothesis(RuleParameters().withIndices(0)(0)(1)) // FIXME shouldn't it be 0?
-      ),
+      )
+    )
+  }
+
+  test("right not") {
+    checkProof(
       Proof(
         () |- (!a, a)
       )(
         RuleIntroductionRightNot(RuleParameters().withIndices(0)()(0)),
         RuleHypothesis(RuleParameters().withIndices(0)(0)(0))
-      ),
+      )
+    )
+  }
+
+  test("left =") {
+    checkProof(
       Proof(
         () |- (t === t)
       )(
         RuleEliminationLeftRefl(RuleParameters().withFunction(Notations.s, t)),
         RuleHypothesis()
-      ),
+      )
+    )
+  }
+
+  test("right =") {
+    checkProof(
       Proof(
         () |- (t === t)
       )(
@@ -118,7 +178,7 @@ class ProofTests extends AnyFunSuite {
   }
 
   test("introduction higher order") {
-    checkProofs(
+    checkProof(
       Proof(
         forall(x, u === x) |- (u === s)
       )(
@@ -128,7 +188,12 @@ class ProofTests extends AnyFunSuite {
             .withFunction(Notations.t, s)
         ),
         RuleHypothesis()
-      ),
+      )
+    )
+  }
+
+  test("right forall right or") {
+    checkProof(
       Proof(
         a |- forall(x, (u === x) \/ a)
       )(
@@ -138,7 +203,12 @@ class ProofTests extends AnyFunSuite {
         ),
         RuleIntroductionRightOr(),
         RuleHypothesis()
-      ),
+      )
+    )
+  }
+
+  test("left exists left and") {
+    checkProof(
       Proof(
         exists(x, (s === x) /\ a) |- a
       )(
@@ -148,7 +218,12 @@ class ProofTests extends AnyFunSuite {
         ),
         RuleIntroductionLeftAnd(),
         RuleHypothesis()
-      ),
+      )
+    )
+  }
+
+  test("right exists") {
+    checkProof(
       Proof(
         (s === t) |- exists(x, s === x)
       )(
@@ -158,7 +233,12 @@ class ProofTests extends AnyFunSuite {
             .withFunction(Notations.t, t)
         ),
         RuleHypothesis()
-      ),
+      )
+    )
+  }
+
+  test("left subst =") {
+    checkProof(
       Proof(
         (s === t, u === t) |- (u === s)
       )(
@@ -167,7 +247,12 @@ class ProofTests extends AnyFunSuite {
             .withPredicate(Notations.p, u === _)
         ),
         RuleHypothesis()
-      ),
+      )
+    )
+  }
+
+  test("right subst =") {
+    checkProof(
       Proof(
         (s === t, u === s) |- (u === t)
       )(
@@ -176,7 +261,12 @@ class ProofTests extends AnyFunSuite {
             .withPredicate(Notations.p, u === _)
         ),
         RuleHypothesis()
-      ),
+      )
+    )
+  }
+
+  test("left subst iff") {
+    checkProof(
       Proof(
         (a <=> b, c <=> b) |- (c <=> a)
       )(
@@ -185,7 +275,12 @@ class ProofTests extends AnyFunSuite {
             .withConnector(Notations.f, c <=> _)
         ),
         RuleHypothesis()
-      ),
+      )
+    )
+  }
+
+  test("right subst iff") {
+    checkProof(
       Proof(
         (a <=> b, c <=> a) |- (c <=> b)
       )(
@@ -196,12 +291,10 @@ class ProofTests extends AnyFunSuite {
         RuleHypothesis()
       )
     )
-
-    // TODO remaining rules
   }
 
-  test("elimination rules") {
-    checkProofs(
+  test("elimination left subst iff") {
+    checkProof(
       Proof(
         (s === t) |- (t === s)
       )(
@@ -214,7 +307,12 @@ class ProofTests extends AnyFunSuite {
         RuleHypothesis(),
         TacticalRewrite((s === t) |- (s === t)),
         RuleHypothesis()
-      ),
+      )
+    )
+  }
+
+  test("elimination right subst iff") {
+    checkProof(
       Proof(
         (s === t) |- (t === s)
       )(
@@ -227,7 +325,12 @@ class ProofTests extends AnyFunSuite {
         RuleHypothesis(),
         TacticalRewrite((s === t) |- (s === t)),
         RuleHypothesis()
-      ),
+      )
+    )
+  }
+
+  test("elimination left subst =") {
+    checkProof(
       Proof(
         (s === t, t === u) |- (s === u)
       )(
@@ -239,7 +342,12 @@ class ProofTests extends AnyFunSuite {
         ),
         RuleHypothesis(),
         RuleHypothesis()
-      ),
+      )
+    )
+  }
+
+  test("elimination right subst =") {
+    checkProof(
       Proof(
         (s === t, t === u) |- (s === u)
       )(
@@ -279,8 +387,6 @@ class ProofTests extends AnyFunSuite {
 
     val reconstructed = reconstructSCProofForTheorem(thm3)
 
-    println(Printer.prettySCProof(reconstructed))
-
-    assert(SCProofChecker.checkSCProof(reconstructed).isValid)
+    assert(SCProofChecker.checkSCProof(reconstructed).isValid, Printer.prettySCProof(reconstructed))
   }
 }