From 672131b1d77204667fd6da4c172fdc10f88a735b Mon Sep 17 00:00:00 2001
From: Simon Guilloud <simon.guilloud@bluewin.ch>
Date: Thu, 3 Oct 2024 16:07:58 +0200
Subject: [PATCH 1/3] Update project to scala version 3.5.1. Rewrite
 depreciated syntax. Hide scallion warning report.

---
 build.sbt                                     | 13 ++--
 lisa-examples/src/main/scala/Lattices.scala   | 24 +++----
 .../main/scala/lisa/automation/Apply.scala    |  2 +-
 .../scala/lisa/automation/CommonTactics.scala |  8 +--
 .../scala/lisa/automation/Substitution.scala  | 10 +--
 .../maths/settheory/types/TypeSystem.scala    | 66 ++++++++++---------
 .../maths/settheory/types/adt/Frontend.scala  |  6 +-
 .../maths/settheory/types/adt/Helpers.scala   |  2 +-
 .../maths/settheory/types/adt/Tactics.scala   |  8 +--
 .../maths/settheory/types/adt/Untyped.scala   | 14 ++--
 .../src/main/scala/lisa/fol/Common.scala      | 49 +++++++-------
 .../src/main/scala/lisa/fol/Lambdas.scala     |  2 +-
 .../src/main/scala/lisa/fol/Sequents.scala    |  2 +-
 .../scala/lisa/prooflib/BasicStepTactic.scala |  4 +-
 .../scala/lisa/prooflib/ProofsHelpers.scala   |  2 +-
 .../scala/lisa/utils/parsing/Parser.scala     |  3 +-
 .../lisa/utils/parsing/ParsingUtils.scala     |  2 +-
 .../scala/lisa/kernel/SubstitutionTest.scala  |  3 +
 18 files changed, 117 insertions(+), 103 deletions(-)

diff --git a/build.sbt b/build.sbt
index a38f440c5..256dc91ba 100644
--- a/build.sbt
+++ b/build.sbt
@@ -15,14 +15,15 @@ ThisBuild / javacOptions ++= Seq("-encoding", "UTF-8")
 ThisBuild / semanticdbEnabled := true
 ThisBuild / semanticdbVersion := scalafixSemanticdb.revision
 
+
+
+val scala2 = "2.13.8"
+val scala3 = "3.5.1"
 val commonSettings = Seq(
-  crossScalaVersions := Seq("3.3.3"),
+  crossScalaVersions := Seq(scala3),
   run / fork := true
 )
 
-val scala2 = "2.13.8"
-val scala3 = "3.3.3"
-
 val commonSettings2 = commonSettings ++ Seq(
   scalaVersion := scala2,
   scalacOptions ++= Seq("-Ypatmat-exhaust-depth", "50")
@@ -31,6 +32,8 @@ val commonSettings3 = commonSettings ++ Seq(
   scalaVersion := scala3,
   scalacOptions ++= Seq(
     "-language:implicitConversions",
+    //"-rewrite", "-source", "3.4-migration",
+    "-Wconf:msg=.*will never be selected.*:silent"
   ),
   javaOptions += "-Xmx10G",
   libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.18" % "test",
@@ -49,6 +52,8 @@ lazy val silex = githubProject("https://github.com/epfl-lara/silex.git", "fc07a8
 lazy val customTstpParser = githubProject("https://github.com/SimonGuilloud/scala-tptp-parser.git", "eae9c1b7a9546f74779d77ff50fa6e8a1654cfa0")
 
 scallion/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
+scallion/scalacOptions += "-Wconf:any:silent"
+
 silex/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
 
 lazy val root = Project(
diff --git a/lisa-examples/src/main/scala/Lattices.scala b/lisa-examples/src/main/scala/Lattices.scala
index be45953c8..da63bfb67 100644
--- a/lisa-examples/src/main/scala/Lattices.scala
+++ b/lisa-examples/src/main/scala/Lattices.scala
@@ -33,35 +33,35 @@ object Lattices extends lisa.Main {
   val reflexivity = Axiom(x <= x)
   val antisymmetry = Axiom(((x <= y) /\ (y <= x)) ==> (x === y))
   val transitivity = Axiom(((x <= y) /\ (y <= z)) ==> (x <= z))
-  val lub = Axiom(((x <= z) /\ (y <= z)) <=> ((x u y) <= z))
-  val glb = Axiom(((z <= x) /\ (z <= y)) <=> (z <= (x n y)))
+  val lub = Axiom(((x <= z) /\ (y <= z)) <=> ((x `u` y) <= z))
+  val glb = Axiom(((z <= x) /\ (z <= y)) <=> (z <= (x `n` y)))
 
   // Let's prove some properties !
 
-  val joinLowerBound = Theorem((x <= (x u y)) /\ (y <= (x u y))) {
-    have(thesis) by Tautology.from(lub of (z := (x u y)), reflexivity of (x := (x u y)))
+  val joinLowerBound = Theorem((x <= (x `u` y)) /\ (y <= (x `u` y))) {
+    have(thesis) by Tautology.from(lub of (z := (x `u` y)), reflexivity of (x := (x `u` y)))
   }
 
-  val meetUpperBound = Theorem(((x n y) <= x) /\ ((x n y) <= y)) {
+  val meetUpperBound = Theorem(((x `n` y) <= x) /\ ((x `n` y) <= y)) {
     sorry
   }
-  val joinCommutative = Theorem((x u y) === (y u x)) {
-    val s1 = have((x u y) <= (y u x)) by Tautology.from(lub of (z := (y u x)), joinLowerBound of (x := y, y := x))
-    have(thesis) by Tautology.from(s1, s1 of (x := y, y := x), antisymmetry of (x := x u y, y := y u x))
+  val joinCommutative = Theorem((x `u` y) === (y `u` x)) {
+    val s1 = have((x `u` y) <= (y `u` x)) by Tautology.from(lub of (z := (y `u` x)), joinLowerBound of (x := y, y := x))
+    have(thesis) by Tautology.from(s1, s1 of (x := y, y := x), antisymmetry of (x := x `u` y, y := y `u` x))
   }
 
-  val meetCommutative = Theorem((x n y) === (y n x)) {
+  val meetCommutative = Theorem((x `n` y) === (y `n` x)) {
     sorry
   }
-  val joinAbsorption = Theorem((x <= y) |- (x u y) === y) {
+  val joinAbsorption = Theorem((x <= y) |- (x `u` y) === y) {
     sorry
   }
 
-  val meetAbsorption = Theorem((x <= y) |- (x n y) === x) {
+  val meetAbsorption = Theorem((x <= y) |- (x `n` y) === x) {
     sorry
   }
 
-  val joinAssociative = Theorem((x u (y u z)) === ((x u y) u z)) {
+  val joinAssociative = Theorem((x `u` (y `u` z)) === ((x `u` y) `u` z)) {
     sorry
   }
 
diff --git a/lisa-sets/src/main/scala/lisa/automation/Apply.scala b/lisa-sets/src/main/scala/lisa/automation/Apply.scala
index a0c22d790..eb3896284 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Apply.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Apply.scala
@@ -112,7 +112,7 @@ class Apply(using val lib: Library, val proof: lib.Proof)(thm: proof.Fact) exten
     * @param tSubst the assignment for term variables
     */
   private def substitute(using _proof: lib.Proof)(fact: _proof.Fact, fSubst: FormulaSubstitution, tSubst: TermSubstitution): _proof.Fact =
-    fact.of(fSubst.toFSubstPair: _*).of(tSubst.toTSubstPair: _*)
+    fact.of(fSubst.toFSubstPair*).of(tSubst.toTSubstPair*)
 
   /**
   * Applies on method with a varargs instead of a sequence.
diff --git a/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
index c5b8e80a2..a81e8d9ac 100644
--- a/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
@@ -178,14 +178,14 @@ object CommonTactics {
 
           // Instantiate terms in the definition
           val subst = vars.zip(xs).map(tup => tup._1 := tup._2)
-          val P = definition.f.substitute(subst: _*)
+          val P = definition.f.substitute(subst*)
           val expected = P.substitute(y := fxs)
           if (!F.isSame(expected, bot.right.head)) {
             return proof.InvalidProofTactic("Right-hand side of bottom sequent should be of the form P(f(xs)).")
           }
 
           TacticSubproof {
-            lib.have(F.∀(y, (y === fxs) <=> P)) by Tautology.from(uniqueness, definition.of(subst: _*))
+            lib.have(F.∀(y, (y === fxs) <=> P)) by Tautology.from(uniqueness, definition.of(subst*))
             lib.thenHave((y === fxs) <=> P) by InstantiateForall(y)
             lib.thenHave((fxs === fxs) <=> P.substitute(y := fxs)) by InstFunSchema(Map(y -> fxs))
             lib.thenHave(P.substitute(y := fxs)) by Restate
@@ -218,7 +218,7 @@ object CommonTactics {
           // val instantiations: Seq[(F.SchematicTermLabel, F.LambdaTermTerm)] = vars.zip(xs.map(x => F.LambdaTermTerm(Seq(), x)))
 
           val subst = vars.zip(xs).map(tup => tup._1 := tup._2)
-          val P = definition.f.substitute(subst: _*)
+          val P = definition.f.substitute(subst*)
           // Instantiate terms in the definition
           // val P = F.LambdaTermFormula(Seq(y), expr(xs))
 
@@ -248,7 +248,7 @@ object CommonTactics {
           }
 
           TacticSubproof {
-            lib.have(F.∀(y, (y === fxs) <=> P)) by Tautology.from(uniqueness, definition.of(subst: _*))
+            lib.have(F.∀(y, (y === fxs) <=> P)) by Tautology.from(uniqueness, definition.of(subst*))
             lib.thenHave((y === fxs) <=> P) by InstantiateForall(y)
             lib.thenHave((fxs === fxs) <=> P.substitute(y := fxs)) by InstFunSchema(Map(y -> fxs))
             lib.thenHave(P.substitute(y := fxs)) by Restate
diff --git a/lisa-sets/src/main/scala/lisa/automation/Substitution.scala b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
index fcc456429..87eab43cd 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
@@ -42,7 +42,7 @@ object Substitution {
 
       // make sure substitutions are all valid
       val violatingSubstitutions = substitutions.collect {
-        case f: proof.Fact if !validRule(f) => proof.sequentOfFact(f)
+        case f : proof.Fact @unchecked if !validRule(f) => proof.sequentOfFact(f)
         case j: lib.JUSTIFICATION if !validRule(j) => j.statement
       }
 
@@ -236,7 +236,7 @@ object Substitution {
               leftContextReduced.termRules.map { case (_, (rule, subst)) =>
                 sourceOf.get(rule) match {
                   case Some(f: proof.Fact) =>
-                    f.of(subst.toSeq.map((l, r) => (l := r)): _*)
+                    f.of(subst.toSeq.map((l, r) => (l := r))*)
                   // case Some(j: lib.theory.Justification) =>
                   //   j.of(subst.toSeq.map((l, r) => (l, lambda(Seq(), r))): _*)
                   case _ =>
@@ -246,7 +246,7 @@ object Substitution {
                 leftContextReduced.formulaRules.map { case (_, (rule, subst)) =>
                   sourceOf.get(rule) match {
                     case Some(f: proof.Fact) =>
-                      f.of(subst._1.toSeq.map((l, r) => (l := r)) ++ subst._2.toSeq.map((l, r) => (l := r)): _*)
+                      f.of(subst._1.toSeq.map((l, r) => (l := r)) ++ subst._2.toSeq.map((l, r) => (l := r))*)
                     // case Some(j: lib.theory.Justification) =>
                     //   j.of(subst._1.toSeq.map((l, r) => (l, lambda(Seq[Variable](), r))) ++ subst._2.toSeq.map((l, r) => (l, lambda(Seq[Variable](), r))): _*)
                     case _ =>
@@ -257,7 +257,7 @@ object Substitution {
               rightContextReduced.termRules.map { case (_, (rule, subst)) =>
                 sourceOf.get(rule) match {
                   case Some(f: proof.Fact) =>
-                    f.of(subst.toSeq.map((l, r) => (l := r)): _*)
+                    f.of(subst.toSeq.map((l, r) => (l := r))*)
                   // case Some(j: lib.theory.Justification) =>
                   //   j.of(subst.toSeq.map((l, r) => (l, lambda(Seq(), r))): _*)
                   case None =>
@@ -267,7 +267,7 @@ object Substitution {
                 rightContextReduced.formulaRules.map { case (_, (rule, subst)) =>
                   sourceOf.get(rule) match {
                     case Some(f: proof.Fact) =>
-                      f.of(subst._1.toSeq.map((l, r) => (l := r)) ++ subst._2.toSeq.map((l, r) => (l := r)): _*)
+                      f.of(subst._1.toSeq.map((l, r) => (l := r)) ++ subst._2.toSeq.map((l, r) => (l := r))*)
                     // case Some(j: lib.theory.Justification) =>
                     //   j.of(subst._1.toSeq.map((l, r) => (l, lambda(Seq[Variable](), r))) ++ subst._2.toSeq.map((l, r) => (l, lambda(Seq[Variable](), r))): _*)
                     case None =>
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala
index 850103caa..e85f6e233 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala
@@ -13,6 +13,8 @@ import lisa.maths.settheory.SetTheory.functional
 import lisa.prooflib.OutputManager
 import lisa.maths.settheory.SetTheory.{singleton, app}
 
+import annotation.nowarn
+
 object TypeLib extends lisa.Main {
 
   import TypeSystem.*
@@ -40,7 +42,7 @@ object TypeLib extends lisa.Main {
   // C |> D is the functional class of functionals from the class C to the class D
   // F is C |> D desugars into ∀(x, (x is C) => (F(x) is D))
 
-  val testTheorem = Theorem((x is A, f is (A |=> B), F is (A |=> B) |> (A |=> B) ) |- (F(f)*(x) is B)) {
+  val testTheorem = Theorem((x `is` A, f `is` (A |=> B), F `is` (A |=> B) |> (A |=> B) ) |- (F(f)*(x) `is` B)) {
     have(thesis) by TypeChecker.prove
   }
 
@@ -87,7 +89,7 @@ object TypeSystem  {
 
   case class FunctionalClass(in: Seq[Class], args: Seq[Variable], out: Class, arity: Int) {
     def formula[N <: Arity](f: (Term**N |-> Term)): Formula = 
-      val inner = (args.zip(in.toSeq).map((term, typ) => (term is typ).asFormula).reduceLeft((a, b) => a /\ b)) ==> (f.applySeq(args) is out)
+      val inner = (args.zip(in.toSeq).map((term, typ) => (term `is` typ).asFormula).reduceLeft((a, b) => a /\ b)) ==> (f.applySeq(args) `is` out)
       args.foldRight(inner)((v, form) => forall(v, form))
 
     override def toString(): String = in.map(_.toStringSeparated()).mkString("(", ", ", ")") + " |> " + out.toStringSeparated()
@@ -112,8 +114,8 @@ object TypeSystem  {
   }
 
   extension [A <: Class](t: Term) {
-    def is(clas:A): Formula with TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula with TypeAssignment[A]]
-    def ::(clas:A): Formula with TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula with TypeAssignment[A]]
+    def is(clas:A): Formula & TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula & TypeAssignment[A]]
+    def ::(clas:A): Formula & TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula & TypeAssignment[A]]
     def @@(t2: Term): AppliedFunction = AppliedFunction(t, t2)
     def *(t2: Term): AppliedFunction = AppliedFunction(t, t2)
   }
@@ -220,7 +222,7 @@ object TypeSystem  {
 
     def unapply[N <: Arity](f: Formula): Option[((Term ** N) |-> Term, FunctionalClass)] = 
       f match 
-        case ta: FunctionalTypeAssignment[N] => Some((ta.functional, ta.typ))
+        case ta: FunctionalTypeAssignment[N] @unchecked => Some((ta.functional, ta.typ))
         case _ => None
   }
   private class FunctionalTypeAssignmentConstant[N <: Arity](val functional: Term**N |-> Term, val typ: FunctionalClass, formula: ConstantFormula) extends ConstantFormula(formula.id) with FunctionalTypeAssignment[N]
@@ -310,15 +312,19 @@ object TypeSystem  {
       new TypedSimpleConstantDefinition(fullName, line, file)(expression, out, defThm, typ)
     }
   }
+
+  
   extension (d: definitionWithVars[0]) {
+    @nowarn
     inline infix def -->[A<:Class](
           using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(term:Term, typ: A): TypedConstant[A] =
       TypedSimpleConstantDefinition[A](name.value, line.value, file.value)(term, typ).typedLabel
   }
   
+  
   extension (c: Constant) {
     def typedWith[A <: Class](typ:A)(justif: JUSTIFICATION) : TypedConstant[A] = 
-      if justif.statement.right.size != 1  || justif.statement.left.size != 0 || !K.isSame((c is typ).asFormula.underlying, justif.statement.right.head.underlying) then
+      if justif.statement.right.size != 1  || justif.statement.left.size != 0 || !K.isSame((c `is` typ).asFormula.underlying, justif.statement.right.head.underlying) then
         throw new IllegalArgumentException(s"A proof of typing of $c must be of the form ${c :: typ}, but the given justification shows ${justif.statement}.")
       else TypedConstant(c.id, typ, justif)
   }
@@ -345,7 +351,7 @@ object TypeSystem  {
       var typingError: proof.ProofTacticJudgement = null
       bot.right.find(goal =>
         goal match
-          case (term is typ) => 
+          case (term `is` typ) => 
             val ptj = typecheck(using SetTheoryLibrary)(context.toSeq, term, Some(typ))
             if ptj.isValid then
               success = ptj
@@ -378,21 +384,21 @@ object TypeSystem  {
           def innerTypecheck(context2: Map[Term, Seq[Class]], term:Term, typ:Option[Class]): Class= {
             val possibleTypes = typingAssumptions.getOrElse(term, Nil)
             if typ == Some(any) then 
-              have(term is any) by Restate.from(TypeLib.any.definition of (x := term))
+              have(term `is` any) by Restate.from(TypeLib.any.definition of (x := term))
               any
             else if typ.isEmpty && possibleTypes.size >=1 then
-              have(term is possibleTypes.head) by Restate
+              have(term `is` possibleTypes.head) by Restate
               possibleTypes.head
             else if (typ.nonEmpty && possibleTypes.contains(typ.get)) then
-              have(term is typ.get) by Restate
+              have(term `is` typ.get) by Restate
               typ.get
             else term match
               case tc: TypedConstant[?] => 
                 if typ.isEmpty then
-                  have(tc is tc.typ) by Restate.from(tc.justif)
+                  have(tc `is` tc.typ) by Restate.from(tc.justif)
                   tc.typ
-                else if K.isSame((tc is typ.get).asFormula.underlying, (tc is tc.typ).asFormula.underlying) then
-                  have(tc is typ.get) by Restate.from(tc.justif)
+                else if K.isSame((tc `is` typ.get).asFormula.underlying, (tc `is` tc.typ).asFormula.underlying) then
+                  have(tc `is` typ.get) by Restate.from(tc.justif)
                   typ.get
                 else throw TypingException("Constant " + tc + " expected to be of type " + typ + " but has type " + tc.typ + ".")
 
@@ -404,8 +410,8 @@ object TypeSystem  {
                 funcType match
                   case inType |=> outType => typ match
                     case None => 
-                      if K.isSame((arg is inType).asFormula.underlying, (arg is argType).asFormula.underlying) then
-                        have(term is outType) by Tautology.from(
+                      if K.isSame((arg `is` inType).asFormula.underlying, (arg `is` argType).asFormula.underlying) then
+                        have(term `is` outType) by Tautology.from(
                           funcspaceAxiom of (f := func, x := arg, A:= inType, B:= outType),
                           funcProof,
                             argProof
@@ -413,9 +419,9 @@ object TypeSystem  {
                         outType
                       else throw 
                         TypingException("Function " + func + " found to have type " + funcType + ", but argument " + arg + " has type " + argType + " instead of expected " + inType + ".")
-                    case Some(typ) if K.isSame((term is typ).asFormula.underlying, (term is outType).asFormula.underlying) =>
-                      if K.isSame((arg is inType).asFormula.underlying, (arg is argType).asFormula.underlying) then
-                        have(term is outType) by Tautology.from(
+                    case Some(typ) if K.isSame((term `is` typ).asFormula.underlying, (term `is` outType).asFormula.underlying) =>
+                      if K.isSame((arg `is` inType).asFormula.underlying, (arg `is` argType).asFormula.underlying) then
+                        have(term `is` outType) by Tautology.from(
                           funcspaceAxiom of (f := func, x := arg, A:= inType, B:= outType),
                           funcProof,
                             argProof
@@ -450,7 +456,7 @@ object TypeSystem  {
                       labelTypes.find((labelType, step) =>
                         labelType.arity == args.size && 
                         (args zip argTypes).zip(labelType.in.toSeq).forall((argAndTypes, inType) => 
-                          K.isSame((argAndTypes._1 is inType).asFormula.underlying, (argAndTypes._1 is argAndTypes._2).asFormula.underlying) //
+                          K.isSame((argAndTypes._1 `is` inType).asFormula.underlying, (argAndTypes._1 `is` argAndTypes._2).asFormula.underlying) //
                         )
                       ) match 
                         case None =>
@@ -461,28 +467,28 @@ object TypeSystem  {
                           val in: Seq[Class] = labelType.in.toSeq
                           //val labelProp = labelType.formula(label.asInstanceOf)
                           val labelPropStatement = step()
-                          val labInst = labelPropStatement.of(args: _*)
+                          val labInst = labelPropStatement.of(args*)
                           val subst = (labelType.args zip args).map((v, a) => (v := a))
                           val newOut: Class = out match {
-                            case t: Term => t.substitute(subst: _*)
-                            case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst: _*)
+                            case t: Term => t.substitute(subst*)
+                            case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst*)
                           }
-                          have(term is newOut) by Tautology.from(
-                            (argTypesProofs :+ labInst ) : _*
+                          have(term `is` newOut) by Tautology.from(
+                            (argTypesProofs :+ labInst )*
                           )
                           newOut
                     case Some(typValue) => 
                       labelTypes.find((labelType, step) =>
                         labelType.arity == args.size && 
                         (args zip argTypes).zip(labelType.in.toSeq).forall((argAndTypes, inType) => 
-                          K.isSame((argAndTypes._1 is inType).asFormula.underlying, (argAndTypes._1 is argAndTypes._2).asFormula.underlying)
+                          K.isSame((argAndTypes._1 `is` inType).asFormula.underlying, (argAndTypes._1 `is` argAndTypes._2).asFormula.underlying)
                         ) && {
                           val subst = (labelType.args zip args).map((v, a) => (v := a))
                           val newOut: Class = labelType.out match {
-                            case t: Term => t.substitute(subst: _*)
-                            case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst: _*)
+                            case t: Term => t.substitute(subst*)
+                            case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst*)
                           }
-                          K.isSame((term is newOut).asFormula.underlying, (term is typValue).asFormula.underlying)
+                          K.isSame((term `is` newOut).asFormula.underlying, (term `is` typValue).asFormula.underlying)
                           
                         }
                       ) match
@@ -493,8 +499,8 @@ object TypeSystem  {
                           val in: Seq[Class] = labelType.in.toSeq
                           //val labelProp = labelType.formula(label.asInstanceOf)
                           val labelPropStatement = step()
-                          have(term is typValue) by Tautology.from(
-                            (argTypesProofs :+ labelPropStatement.of(args: _*) ) : _*
+                          have(term `is` typValue) by Tautology.from(
+                            (argTypesProofs :+ labelPropStatement.of(args*) )*
                           )
                           typValue
 
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala
index df6d157e3..fa455cd39 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala
@@ -201,7 +201,7 @@ object ADTSyntax {
       val semanticCons = trimmedNames.tail.zip(syntacticCons).map(SemanticConstructor(_, _, syntacticADT))
       val semanticADT = SemanticADT[N](syntacticADT, semanticCons)
       val cons = semanticCons.map(Constructor(_)) 
-      (ADT[N](semanticADT, cons), new constructors[N](cons : _*))
+      (ADT[N](semanticADT, cons), new constructors[N](cons*))
   
   }
 
@@ -356,7 +356,7 @@ object ADTSyntax {
       * @param adt the ADT
       * @return a tuple containing the ADT and its constructors
       */
-    private def extractConstructors[N <: Arity](adt: ADT[N]): (ADT[N], constructors[N]) = (adt, constructors(adt.constructors : _*))
+    private def extractConstructors[N <: Arity](adt: ADT[N]): (ADT[N], constructors[N]) = (adt, constructors(adt.constructors*))
 
     /**
       * Outputs a polymorphic ADT and constructors from a user specification
@@ -514,7 +514,7 @@ object ADTSyntax {
       val subst = adtVar -> consTerm
 
       val assumptions = 
-        (wellTypedSet(cons.underlying.semanticSignature(vars).map(p => (p._1, p._2.substitute(cons.underlying.typeVariablesSeq.zip(args).map(SubstPair(_, _)) : _*))))
+        (wellTypedSet(cons.underlying.semanticSignature(vars).map(p => (p._1, p._2.substitute(cons.underlying.typeVariablesSeq.zip(args).map(SubstPair(_, _))*))))
         ++ 
         cons.underlying.syntacticSignature(vars).filter(_._2 == Self).map((v, _) => prop.substitute(adtVar -> v)))
 
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala
index 5830f1aab..604b8c34b 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala
@@ -265,7 +265,7 @@ private[adt] object ADTDefinitions {
     def substitute(p: SubstPair*): ConstructorArgument = 
       this match
         case Self => Self
-        case GroundType(t) => GroundType(t.substitute(p : _*))
+        case GroundType(t) => GroundType(t.substitute(p*))
   }
   
   /**
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala
index cb8250798..7a05b0b49 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala
@@ -47,10 +47,10 @@ class Induction[M <: Arity](expectedVar: Option[Variable], expectedADT: Option[A
 
     val prop = lambda[Term, Formula](x, propFun(x))
     val typeVariablesSubstPairs = adt.typeVariables.toSeq.zip(typeVariablesSubst).map(SubstPair(_, _))
-    val instTerm = adt(typeVariablesSubst : _*)
+    val instTerm = adt(typeVariablesSubst*)
 
-    adt.constructors.foldLeft[proof.Fact](adt.induction.of((typeVariablesSubstPairs :+ (P := prop)): _*)) ( (acc, c) =>
-      val inductiveCaseProof = cases(c)._1.zip(c.underlying.underlying.specification.map(_.substitute(typeVariablesSubstPairs : _*))).foldRight[proof.Fact](cases(c)._2) ( (el, acc2) =>
+    adt.constructors.foldLeft[proof.Fact](adt.induction.of((typeVariablesSubstPairs :+ (P := prop))*)) ( (acc, c) =>
+      val inductiveCaseProof = cases(c)._1.zip(c.underlying.underlying.specification.map(_.substitute(typeVariablesSubstPairs*))).foldRight[proof.Fact](cases(c)._2) ( (el, acc2) =>
         val (v, ty) = el
         val accRight: Formula = acc2.statement.right.head
         ty match 
@@ -140,7 +140,7 @@ class Induction[M <: Arity](expectedVar: Option[Variable], expectedADT: Option[A
 
         val prop = inferedProp.getOrElse(bot.right.head)
         val propFunction = (t: Term) => inferedProp.getOrElse(bot.right.head).substitute(inferedVar -> t)
-        val assignment = inferedVar :: inferedADT(inferedArgs : _*)
+        val assignment = inferedVar :: inferedADT(inferedArgs*)
         val context = (if inferedProp.isDefined then bot else bot -<< assignment).left
         val builder = ADTSyntax.CaseBuilder[N, proof.ProofStep, (Sequent, Seq[Term], Variable)]((context |- prop, inferedArgs, inferedVar))
         cases(using builder)
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala
index 61dd75a7e..cb3944c1a 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala
@@ -375,7 +375,7 @@ private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: source
           // STEP 2.1: Prove that we can expand the domain of the (quantified) variables of the constructor
           val andSeq =
             for (v, ty) <- c.signature2 yield have((subsetST, varsWellTypedS) |- in(v, ty.getOrElse(t))) by Weakening(subsetElimination of (z := v))
-          val expandingDomain = have((subsetST, varsWellTypedS) |- varsWellTypedT) by RightAnd(andSeq: _*)
+          val expandingDomain = have((subsetST, varsWellTypedS) |- varsWellTypedT) by RightAnd(andSeq*)
           val weakeningLabelEq = have(labelEq |- labelEq) by Hypothesis
           have((subsetST, varsWellTypedS, labelEq) |- varsWellTypedT /\ labelEq) by RightAnd(expandingDomain, weakeningLabelEq)
 
@@ -390,7 +390,7 @@ private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: source
     // STEP 3: Prove that this holds for any constructor
     // ? Steps 2 and 3 can be merged and optimized through the repeated use of an external theorem like [[ADTHelperTheorems.unionPreimageMonotonic]]
     if constructors.isEmpty then have((subsetST, isConstructorXS) |- isConstructorXT) by Restate
-    else have((subsetST, isConstructorXS) |- isConstructorXT) by LeftOr(isConstructorXSImpliesT: _*)
+    else have((subsetST, isConstructorXS) |- isConstructorXT) by LeftOr(isConstructorXSImpliesT*)
 
     // STEP 4: Prove the thesis by showing that making the union with the function argument does not change the monotonicity
     thenHave(subsetST |- isConstructorXS ==> isConstructorXT) by RightImplies
@@ -820,7 +820,7 @@ private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: source
               case GroundType(t) =>
                 have((hIsTheHeightFunction, in(n, N) /\ constructorVarsInDomain(c, app(h, n))) |- in(v, t)) by Restate
 
-            have((hIsTheHeightFunction, in(n, N) /\ constructorVarsInDomain(c, app(h, n))) |- constructorVarsInDomain(c, term)) by RightAnd(andSeq: _*)
+            have((hIsTheHeightFunction, in(n, N) /\ constructorVarsInDomain(c, app(h, n))) |- constructorVarsInDomain(c, term)) by RightAnd(andSeq*)
             thenHave((hIsTheHeightFunction, exists(n, in(n, N) /\ constructorVarsInDomain(c, app(h, n)))) |- constructorVarsInDomain(c, term)) by LeftExists
           }
 
@@ -985,7 +985,7 @@ private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: source
                   for (v, ty) <- c.signature
                   yield have((hIsTheHeightFunction, in(n, N), constructorVarsInHN) |- in(v, ty.getOrElse(app(h, successor(n))))) by Weakening(liftHeight of (y := v))
 
-                val left = have((hIsTheHeightFunction, in(n, N), constructorVarsInHN) |- constructorVarsInHSuccN) by RightAnd(liftHeightAndSequence: _*)
+                val left = have((hIsTheHeightFunction, in(n, N), constructorVarsInHN) |- constructorVarsInHSuccN) by RightAnd(liftHeightAndSequence*)
                 val right = have(x === c.term |- x === c.term) by Hypothesis
 
                 have((hIsTheHeightFunction, in(n, N), constructorVarsInHN, (x === c.term)) |- constructorVarsInHSuccN /\ (x === c.term )) by RightAnd(
@@ -998,7 +998,7 @@ private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: source
 
               thenHave((hIsTheHeightFunction, in(n, N), isConstructorCXHN) |- isConstructorXHSuccN) by Weakening
 
-          have((hIsTheHeightFunction, in(n, N), isConstructorXHN) |- isConstructorXHSuccN) by LeftOr(liftConstructorHeightOrSequence: _*)
+          have((hIsTheHeightFunction, in(n, N), isConstructorXHN) |- isConstructorXHSuccN) by LeftOr(liftConstructorHeightOrSequence*)
 
       // STEP 1.5: Show that x ∈ introductionFunction(height(n + 1)) => for some c, x = c(x1, ..., xn)
       // with xi, ..., xj ∈ height(n + 1).
@@ -1156,7 +1156,7 @@ private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: source
             ).toSeq
 
 
-          have((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N), inductionFormulaN, isConstructor(x, app(h, n))) |- P(x)) by LeftOr(orSeq: _*)
+          have((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N), inductionFormulaN, isConstructor(x, app(h, n))) |- P(x)) by LeftOr(orSeq*)
       }
 
       // STEP 2.2: Prove that if x ∈ height(n + 1) then P(x) holds.
@@ -1734,7 +1734,7 @@ private class SemanticConstructor[N <: Arity](using line: sourcecode.Line, file:
               have(!inductionPreconditionIneq(c) |- isConstructorMap(c)) by Cut(conditionStrenghtening, lastStep)
               thenHave(!inductionPreconditionIneq(c) |- isConstructor) by Weakening
 
-          have(thesis) by LeftOr(negInductionPreconditionsOrSequence: _*)
+          have(thesis) by LeftOr(negInductionPreconditionsOrSequence*)
       }
 
       // STEP 2: Conclude
diff --git a/lisa-utils/src/main/scala/lisa/fol/Common.scala b/lisa-utils/src/main/scala/lisa/fol/Common.scala
index 77977eb2a..ab09773d5 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Common.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Common.scala
@@ -79,7 +79,7 @@ trait Common {
      * Substitution in the LisaObject of schematics symbols by values. It is not guaranteed by the type system that types of schematics and values match, and the substitution can fail if that is the case.
      * This is the substitution function that should be implemented.
      */
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): T
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): T
     def substituteUnsafe2[A <: SchematicLabel[?], B <: LisaObject[B]](map: Map[A, B]): T = substituteUnsafe(map.asInstanceOf)
 
     /**
@@ -87,7 +87,7 @@ trait Common {
      * This is the substitution that should be used when writing proofs.
      */
     def substitute(pairs: SubstPair*): T = {
-      substituteUnsafe(Map(pairs.map(s => (s._1, (s._2: LisaObject[_])))*))
+      substituteUnsafe(Map(pairs.map(s => (s._1, (s._2: LisaObject[?])))*))
     }
     def substituteOne[S <: LisaObject[S]](v: SchematicLabel[S], arg: S): T = substituteUnsafe(Map(v -> arg))
 
@@ -219,7 +219,7 @@ trait Common {
   sealed trait ConstantTermLabel[A <: (Term | (Seq[Term] |-> Term)) & LisaObject[A]] extends TermLabel[A] with ConstantLabel[A] {
     this: A & LisaObject[A] =>
     val underlyingLabel: K.ConstantFunctionLabel
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantTermLabel[A]
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): ConstantTermLabel[A]
     override def rename(newid: Identifier): ConstantTermLabel[A]
     def freshRename(taken: Iterable[Identifier]): ConstantTermLabel[A]
   }
@@ -276,7 +276,7 @@ trait Common {
    */
   sealed trait FunctionLabel[N <: Arity] extends TermLabel[(Term ** N) |-> Term] with ((Term ** N) |-> Term) {
     val underlyingLabel: K.TermLabel
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): (Term ** N) |-> Term
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): (Term ** N) |-> Term
     def applyUnsafe(args: (Term ** N)): Term = AppliedFunctional(this, args.toSeq)
     override def rename(newid: Identifier): FunctionLabel[N]
     def freshRename(taken: Iterable[Identifier]): FunctionLabel[N]
@@ -293,7 +293,7 @@ trait Common {
     val underlyingLabel: K.VariableLabel = K.VariableLabel(id)
     val underlying = K.VariableTerm(underlyingLabel)
     def applyUnsafe(args: Term ** 0) = this
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Term = {
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): Term = {
       map.get(this) match {
         case Some(subst) =>
           subst match {
@@ -344,7 +344,7 @@ trait Common {
     val underlyingLabel: K.ConstantFunctionLabel = K.ConstantFunctionLabel(id, 0)
     val underlying = K.Term(underlyingLabel, Seq.empty)
     def applyUnsafe(args: Term ** 0) = this
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Constant = this
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): Constant = this
     def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
     def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
     def rename(newid: Identifier): Constant = Constant(newid)
@@ -387,7 +387,7 @@ trait Common {
       case _ => Seq.empty
     }
     @nowarn("msg=the type test for.*cannot be checked at runtime because its type arguments")
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ((Term ** N) |-> Term) = {
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): ((Term ** N) |-> Term) = {
       map.get(this) match {
         case Some(subst) =>
           subst match {
@@ -408,10 +408,9 @@ trait Common {
     def canEqual(that: Any): Boolean =
       that.isInstanceOf[SchematicFunctionLabel[?]]
 
-    // Intentionally avoiding the call to super.equals because no ancestor has overridden equals (see note 7 below)
     override def equals(that: Any): Boolean =
       that match {
-        case other: SchematicFunctionLabel[N] =>
+        case other: SchematicFunctionLabel[_] =>
           ((this eq other) // optional, but highly recommended sans very specific knowledge about this exact class implementation
           || (other.canEqual(this) // optional only if this class is marked final
             && (hashCode == other.hashCode) // optional, exceptionally execution efficient if hashCode is cached, at an obvious space inefficiency tradeoff
@@ -441,7 +440,7 @@ trait Common {
       case AppliedFunctional(label, args) if (label == this) => args
       case _ => Seq.empty
     }
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantFunctionLabel[N] = this
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): ConstantFunctionLabel[N] = this
     def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
     def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
     def rename(newid: Identifier): ConstantFunctionLabel[N] = ConstantFunctionLabel(newid, arity)
@@ -457,7 +456,7 @@ trait Common {
     // Intentionally avoiding the call to super.equals because no ancestor has overridden equals (see note 7 below)
     override def equals(that: Any): Boolean =
       that match {
-        case other: ConstantFunctionLabel[N] =>
+        case other: ConstantFunctionLabel[_] =>
           ((this eq other) // optional, but highly recommended sans very specific knowledge about this exact class implementation
           || (other.canEqual(this) // optional only if this class is marked final
             && (hashCode == other.hashCode) // optional, exceptionally execution efficient if hashCode is cached, at an obvious space inefficiency tradeoff
@@ -486,7 +485,7 @@ trait Common {
    */
   class AppliedFunctional(val label: FunctionLabel[?], val args: Seq[Term]) extends Term with Absolute {
     override val underlying = K.Term(label.underlyingLabel, args.map(_.underlying))
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Term =
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): Term =
       label.substituteUnsafe(map).applyUnsafe(args.map[Term]((x: Term) => x.substituteUnsafe(map)))
 
     def freeSchematicLabels: Set[SchematicLabel[?]] = label.freeSchematicLabels ++ args.flatMap(_.freeSchematicLabels)
@@ -567,7 +566,7 @@ trait Common {
   sealed trait ConstantAtomicLabel[A <: (Formula | (Seq[Term] |-> Formula)) & LisaObject[A]] extends AtomicLabel[A] with ConstantLabel[A] {
     this: A & LisaObject[A] =>
     val underlyingLabel: K.ConstantAtomicLabel
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantAtomicLabel[A]
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): ConstantAtomicLabel[A]
     override def rename(newid: Identifier): ConstantAtomicLabel[A]
     def freshRename(taken: Iterable[Identifier]): ConstantAtomicLabel[A]
   }
@@ -628,7 +627,7 @@ trait Common {
    */
   sealed trait PredicateLabel[N <: Arity] extends AtomicLabel[(Term ** N) |-> Formula] with ((Term ** N) |-> Formula) with Absolute {
     val underlyingLabel: K.AtomicLabel
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): (Term ** N) |-> Formula
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): (Term ** N) |-> Formula
     def applyUnsafe(args: (Term ** N)): Formula = AppliedPredicate(this, args.toSeq)
     override def rename(newid: Identifier): PredicateLabel[N]
     def freshRename(taken: Iterable[Identifier]): PredicateLabel[N]
@@ -645,7 +644,7 @@ trait Common {
     val underlyingLabel: K.VariableFormulaLabel = K.VariableFormulaLabel(id)
     val underlying = K.AtomicFormula(underlyingLabel, Seq.empty)
     def applyUnsafe(args: Term ** 0): Formula = this
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Formula = {
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): Formula = {
       map.get(this) match {
         case Some(subst) =>
           subst match {
@@ -674,7 +673,7 @@ trait Common {
     val underlyingLabel: K.ConstantAtomicLabel = K.ConstantAtomicLabel(id, 0)
     val underlying = K.AtomicFormula(underlyingLabel, Seq.empty)
     def applyUnsafe(args: Term ** 0): Formula = this
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantFormula = this
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): ConstantFormula = this
     def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
     def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
     def rename(newid: Identifier): ConstantFormula = ConstantFormula(newid)
@@ -694,7 +693,7 @@ trait Common {
       case _ => Seq.empty
     }
     @nowarn("msg=the type test for.*cannot be checked at runtime because its type arguments")
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): |->[Term ** N, Formula] = {
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): |->[Term ** N, Formula] = {
       map.get(this) match {
         case Some(subst) =>
           subst match {
@@ -723,7 +722,7 @@ trait Common {
       case AppliedPredicate(label, args) if (label == this) => args
       case _ => Seq.empty
     }
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantPredicateLabel[N] = this
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): ConstantPredicateLabel[N] = this
     def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
     def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
     def rename(newid: Identifier): ConstantPredicateLabel[N] = ConstantPredicateLabel(newid, arity)
@@ -744,7 +743,7 @@ trait Common {
    */
   case class AppliedPredicate(label: PredicateLabel[?], args: Seq[Term]) extends AtomicFormula with Absolute {
     override val underlying = K.AtomicFormula(label.underlyingLabel, args.map(_.underlying))
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Formula =
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): Formula =
       label.substituteUnsafe(map).applyUnsafe(args.map[Term]((x: Term) => x.substituteUnsafe(map)))
 
     def freeSchematicLabels: Set[SchematicLabel[?]] = label.freeSchematicLabels ++ args.toSeq.flatMap(_.freeSchematicLabels)
@@ -769,7 +768,7 @@ trait Common {
     def applySeq(args: Seq[Formula]): Formula = applyUnsafe(args)
     def rename(newid: Identifier): ConnectorLabel
     def freshRename(taken: Iterable[Identifier]): ConnectorLabel
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): |->[Seq[Formula], Formula]
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): |->[Seq[Formula], Formula]
     def mkString(args: Seq[Formula]): String
     def mkStringSeparated(args: Seq[Formula]): String
 
@@ -786,7 +785,7 @@ trait Common {
       case _ => Seq.empty
     }
     @nowarn("msg=the type test for.*cannot be checked at runtime because its type arguments")
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): |->[Formula ** N, Formula] = {
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): |->[Formula ** N, Formula] = {
       map.get(this) match {
         case Some(subst) =>
           subst match {
@@ -820,7 +819,7 @@ trait Common {
       case AppliedConnector(label, args) if (label == this) => args
       case _ => Seq.empty
     }
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type = this
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): this.type = this
     def applyUnsafe(args: Formula ** N): Formula = AppliedConnector(this, args.toSeq)
     def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
     def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
@@ -837,7 +836,7 @@ trait Common {
    */
   case class AppliedConnector(label: ConnectorLabel, args: Seq[Formula]) extends Formula with Absolute {
     override val underlying = K.ConnectorFormula(label.underlyingLabel, args.map(_.underlying))
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Formula =
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): Formula =
       label.applyUnsafe(args.map[Formula]((x: Formula) => x.substituteUnsafe(map)))
     def freeSchematicLabels: Set[SchematicLabel[?]] = label.freeSchematicLabels ++ args.flatMap(_.freeSchematicLabels)
     def allSchematicLabels: Set[SchematicLabel[?]] = label.allSchematicLabels ++ args.flatMap(_.allSchematicLabels)
@@ -872,7 +871,7 @@ trait Common {
     }
     inline def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
     inline def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
-    inline def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type = this
+    inline def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): this.type = this
     override def toString() = id
 
   }
@@ -885,7 +884,7 @@ trait Common {
 
     def allSchematicLabels: Set[Common.this.SchematicLabel[?]] = body.allSchematicLabels + bound
     def freeSchematicLabels: Set[Common.this.SchematicLabel[?]] = body.freeSchematicLabels - bound
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): BinderFormula = {
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): BinderFormula = {
       val newSubst = map - bound
       if (map.values.flatMap(_.freeSchematicLabels).toSet.contains(bound)) {
         val taken: Set[SchematicLabel[?]] = body.allSchematicLabels ++ map.keys
diff --git a/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala b/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala
index bfc152375..45d1f8689 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala
@@ -34,7 +34,7 @@ trait Lambdas extends Common {
      * @param map
      * @return
      */
-    def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): LambdaExpression[T, R, N] = {
+    def substituteUnsafe(map: Map[SchematicLabel[?], LisaObject[?]]): LambdaExpression[T, R, N] = {
       val newSubst = map -- seqBounds
       val conflict = map.values.flatMap(_.freeSchematicLabels).toSet.intersect(bounds.toSet.asInstanceOf)
       if (conflict.nonEmpty) {
diff --git a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
index 792c75aa1..7c8b4f355 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
@@ -30,7 +30,7 @@ trait Sequents extends Common with lisa.fol.Lambdas with Predef {
      * @param map
      * @return
      */
-    def instantiateWithProof(map: Map[SchematicLabel[_], _ <: LisaObject[_]], index: Int): (Sequent, Seq[K.SCProofStep]) = {
+    def instantiateWithProof(map: Map[SchematicLabel[?], ? <: LisaObject[?]], index: Int): (Sequent, Seq[K.SCProofStep]) = {
 
       val mTerm: Map[SchematicFunctionLabel[?] | Variable, LambdaExpression[Term, Term, ?]] =
         map.collect[SchematicFunctionLabel[?] | Variable, LambdaExpression[Term, Term, ?]](p =>
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
index 0501f1b40..899c51da7 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
@@ -187,7 +187,7 @@ object BasicStepTactic {
         else
           proof.InvalidProofTactic("Right-hand side of conclusion is not a superset of the one of the premises.")
       } else if (pivots.forall(_.tail.isEmpty))
-        LeftOr.withParameters(pivots.map(_.head): _*)(premises: _*)(bot)
+        LeftOr.withParameters(pivots.map(_.head)*)(premises*)(bot)
       else
         // some extraneous formulae
         proof.InvalidProofTactic("Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
@@ -586,7 +586,7 @@ object BasicStepTactic {
         else
           proof.InvalidProofTactic("Left-hand side of conclusion is not a superset of the one of the premises.")
       } else if (pivots.forall(_.tail.isEmpty))
-        RightAnd.withParameters(pivots.map(_.head): _*)(premises: _*)(bot)
+        RightAnd.withParameters(pivots.map(_.head)*)(premises*)(bot)
       else
         // some extraneous formulae
         proof.InvalidProofTactic("Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises +φ∧ψ.")
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
index 946a16f2e..00107fc41 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
@@ -122,7 +122,7 @@ trait ProofsHelpers {
   }
 
   extension (using proof: library.Proof)(fact: proof.Fact) {
-    def of(insts: (F.SubstPair | F.Term)*): proof.InstantiatedFact = {
+    infix def of(insts: (F.SubstPair | F.Term)*): proof.InstantiatedFact = {
       proof.InstantiatedFact(fact, insts)
     }
     def statement: F.Sequent = proof.sequentOfFact(fact)
diff --git a/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala
index eb45a0001..806caf3da 100644
--- a/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala
@@ -605,7 +605,7 @@ class Parser(
         infixPredicateLabels ++
         ((and has Associativity.Left) ::
           (or has Associativity.Left) ::
-          (toplevelConnector has Associativity.None) :: Nil): _*
+          (toplevelConnector has Associativity.None) :: Nil)*
     )(
       (l, conn, r) => Termula(conn, Seq(l, r), (l.range._1, r.range._2)),
       {
@@ -640,6 +640,7 @@ class Parser(
         val (id, r) = t match {
           case ConstantToken(id, r) => (id, r)
           case SchematicToken(id, r) => (id, r)
+          case _ => throw UnreachableException
         }
         RangedLabel(VariableFormulaLabel(id), r)
       },
diff --git a/lisa-utils/src/main/scala/lisa/utils/parsing/ParsingUtils.scala b/lisa-utils/src/main/scala/lisa/utils/parsing/ParsingUtils.scala
index 6f1565ab1..858f6abff 100644
--- a/lisa-utils/src/main/scala/lisa/utils/parsing/ParsingUtils.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/parsing/ParsingUtils.scala
@@ -12,7 +12,7 @@ trait ParsingUtils extends Operators { self: Parsers =>
     /**
      * Indicates the associativity of the operator.
      */
-    def has(associativity: lisa.utils.parsing.Associativity): PrecedenceLevel[Op] = PrecedenceLevel(operator, associativity)
+    infix def has(associativity: lisa.utils.parsing.Associativity): PrecedenceLevel[Op] = PrecedenceLevel(operator, associativity)
   }
 
   def singleInfix[Op, A](elem: Syntax[A], op: Syntax[Op])(function: (A, Op, A) => A, inverse: PartialFunction[A, (A, Op, A)] = PartialFunction.empty): Syntax[A] =
diff --git a/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala b/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
index e1ee7a350..b5e59ffc7 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
@@ -144,18 +144,21 @@ class SubstitutionTest extends AnyFunSuite {
     case class $(f: Formula, m: ((SchematicConnectorLabel, LambdaFormulaFormula) | (SchematicAtomicLabel, LambdaTermFormula) | (SchematicTermLabel, LambdaTermTerm))*)
     extension (c: $) {
       inline infix def _VS_(t2: Formula): Assertion = {
+        @annotation.nowarn
         val mCon: Map[SchematicConnectorLabel, LambdaFormulaFormula] = c.m
           .collect({
             case e if e._1.isInstanceOf[SchematicConnectorLabel] => e
           })
           .toMap
           .asInstanceOf
+        @annotation.nowarn
         val mPred: Map[SchematicAtomicLabel, LambdaTermFormula] = c.m
           .collect({
             case e if e._1.isInstanceOf[SchematicAtomicLabel] => e
           })
           .toMap
           .asInstanceOf
+        @annotation.nowarn
         val mTerm: Map[SchematicTermLabel, LambdaTermTerm] = c.m
           .collect({
             case e if e._1.isInstanceOf[SchematicTermLabel] => e

From f643ca91cfe98207c9e862e762feab0db0da77bd Mon Sep 17 00:00:00 2001
From: Simon Guilloud <simon.guilloud@bluewin.ch>
Date: Thu, 3 Oct 2024 16:50:10 +0200
Subject: [PATCH 2/3] update changelist

---
 CHANGES.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 3c8fec63a..fdcd76e10 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,8 @@
 # Change List
 
+## 2024-10-03
+Update to Scala 3.5.1. Silence warnings from scallion and other erroneous ones.
+
 ## 2024-07-22
 Resealed the `Proof` trait following a fix of the relevant compiler bug [scala/scala3#19031](https://github.com/scala/scala3/issues/19031). 
 

From e4eee5084141212ef4d481e0fe9ee2f3fc74ecd4 Mon Sep 17 00:00:00 2001
From: Simon Guilloud <simon.guilloud@bluewin.ch>
Date: Fri, 4 Oct 2024 12:13:12 +0200
Subject: [PATCH 3/3] minonr fix, mark n and u infix in Lattices.scala.

---
 lisa-examples/src/main/scala/Lattices.scala | 28 ++++++++++-----------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/lisa-examples/src/main/scala/Lattices.scala b/lisa-examples/src/main/scala/Lattices.scala
index da63bfb67..cbc4c28ed 100644
--- a/lisa-examples/src/main/scala/Lattices.scala
+++ b/lisa-examples/src/main/scala/Lattices.scala
@@ -21,8 +21,8 @@ object Lattices extends lisa.Main {
   // Enables infix notation
   extension (left: Term) {
     def <=(right: Term): Formula = Lattices.<=.applyUnsafe(Seq(left, right))
-    def u(right: Term): Term = Lattices.u.applyUnsafe(Seq(left, right))
-    def n(right: Term): Term = Lattices.n.applyUnsafe(Seq(left, right))
+    infix def u(right: Term): Term = Lattices.u.applyUnsafe(Seq(left, right))
+    infix def n(right: Term): Term = Lattices.n.applyUnsafe(Seq(left, right))
   }
 
   // We now states the axioms of lattices
@@ -33,35 +33,35 @@ object Lattices extends lisa.Main {
   val reflexivity = Axiom(x <= x)
   val antisymmetry = Axiom(((x <= y) /\ (y <= x)) ==> (x === y))
   val transitivity = Axiom(((x <= y) /\ (y <= z)) ==> (x <= z))
-  val lub = Axiom(((x <= z) /\ (y <= z)) <=> ((x `u` y) <= z))
-  val glb = Axiom(((z <= x) /\ (z <= y)) <=> (z <= (x `n` y)))
+  val lub = Axiom(((x <= z) /\ (y <= z)) <=> ((x u y) <= z))
+  val glb = Axiom(((z <= x) /\ (z <= y)) <=> (z <= (x n y)))
 
   // Let's prove some properties !
 
-  val joinLowerBound = Theorem((x <= (x `u` y)) /\ (y <= (x `u` y))) {
-    have(thesis) by Tautology.from(lub of (z := (x `u` y)), reflexivity of (x := (x `u` y)))
+  val joinLowerBound = Theorem((x <= (x u y)) /\ (y <= (x u y))) {
+    have(thesis) by Tautology.from(lub of (z := (x u y)), reflexivity of (x := (x u y)))
   }
 
-  val meetUpperBound = Theorem(((x `n` y) <= x) /\ ((x `n` y) <= y)) {
+  val meetUpperBound = Theorem(((x n y) <= x) /\ ((x n y) <= y)) {
     sorry
   }
-  val joinCommutative = Theorem((x `u` y) === (y `u` x)) {
-    val s1 = have((x `u` y) <= (y `u` x)) by Tautology.from(lub of (z := (y `u` x)), joinLowerBound of (x := y, y := x))
-    have(thesis) by Tautology.from(s1, s1 of (x := y, y := x), antisymmetry of (x := x `u` y, y := y `u` x))
+  val joinCommutative = Theorem((x u y) === (y u x)) {
+    val s1 = have((x u y) <= (y u x)) by Tautology.from(lub of (z := (y u x)), joinLowerBound of (x := y, y := x))
+    have(thesis) by Tautology.from(s1, s1 of (x := y, y := x), antisymmetry of (x := x u y, y := y u x))
   }
 
-  val meetCommutative = Theorem((x `n` y) === (y `n` x)) {
+  val meetCommutative = Theorem((x n y) === (y n x)) {
     sorry
   }
-  val joinAbsorption = Theorem((x <= y) |- (x `u` y) === y) {
+  val joinAbsorption = Theorem((x <= y) |- (x u y) === y) {
     sorry
   }
 
-  val meetAbsorption = Theorem((x <= y) |- (x `n` y) === x) {
+  val meetAbsorption = Theorem((x <= y) |- (x n y) === x) {
     sorry
   }
 
-  val joinAssociative = Theorem((x `u` (y `u` z)) === ((x `u` y) `u` z)) {
+  val joinAssociative = Theorem((x u (y u z)) === ((x u y) u z)) {
     sorry
   }