diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index 9e17a4f6c411e615f061e5f9275d765e4cce484b..b741d5dbb1004889884c0f347414bdc7deb8f1ab 100644
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -272,9 +272,11 @@ object Printer {
                             case RightNot(_, t1, _) => pretty("Right ¬", t1)
                             case LeftExists(_, t1, _, _) => pretty("Left ∃", t1)
                             case LeftForall(_, t1, _, _, _) => pretty("Left ∀", t1)
+                            case LeftExistsOne(_, t1, _, _) => pretty("Left ∃!", t1)
                             case LeftOr(_, l, _) => pretty("Left ∨", l*)
                             case RightExists(_, t1, _, _, _) => pretty("Right ∃", t1)
                             case RightForall(_, t1, _, _) => pretty("Right ∀", t1)
+                            case RightExistsOne(_, t1, _, _) => pretty("Right ∃!", t1)
                             case RightAnd(_, l, _) => pretty("Right ∧", l*)
                             case RightIff(_, t1, t2, _, _) => pretty("Right ↔", t1, t2)
                             case RightImplies(_, t1, _, _) => pretty("Right →", t1)
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index a67c56156fce6623033c917b3d545e0a35176c7e..0f9c4ce943a8b1976854e559c5d24763976e26ba 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -107,7 +107,7 @@ class RunningTheory {
     def makePredicateDefinition(label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula): RunningTheoryJudgement[this.PredicateDefinition] = {
         if (belongsToTheory(phi))
             if (!isAcceptedPredicateLabel(label))
-                if (phi.freeVariables.isEmpty && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
+                if (phi.freeVariables.subsetOf(args.toSet) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
                     val newDef = PredicateDefinition(label, args, phi)
                     predDefinitions.update(label, Some(newDef))
                     RunningTheoryJudgement.ValidJustification(newDef)
@@ -133,7 +133,7 @@ class RunningTheory {
     def makeFunctionDefinition(proof: SCProof, justifications:Seq[Justification], label: ConstantFunctionLabel, args: Seq[VariableLabel], out: VariableLabel, phi: Formula): RunningTheoryJudgement[this.FunctionDefinition] = {
         if (belongsToTheory(phi))
             if (!isAcceptedFunctionLabel(label))
-                if (phi.freeVariables.isEmpty && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
+                if (phi.freeVariables.subsetOf(args.toSet + out) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
                     if (proof.imports.forall(i => justifications.exists( j => isSameSequent(i, sequentFromJustification(j)))))
                         val r = SCProofChecker.checkSCProof(proof)
                         r match {