isolated theory improvement to push other changes.

src/main/scala/proven/dev/Library.scala

-package proven.dev
-
-import lisa.kernel.fol.FOL
-import lisa.kernel.proof.*
-import utilities.TheoriesHelpers.{*, given}
-import utilities.KernelHelpers.{*, given}
-import lisa.kernel.fol.FOL.*
-
-trait Library {
-    implicit val theory:RunningTheory
-
-    def theorem(name: String, statement:String, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] = theory.theorem(name, statement, proof, justifications)
-
-    val a:String = "a"
-    val b:String = "b"
-    val c:String = "c"
-    val d:String = "d"
-    val e:String = "e"
-    val f:String = "f"
-    val g:String = "g"
-    val h:String = "h"
-    val i:String = "i"
-    val j:String = "j"
-    val k:String = "k"
-    val l:String = "l"
-    val m:String = "m"
-    val n:String = "n"
-    val o:String = "o"
-    val p:String = "p"
-    val q:String = "q"
-    val r:String = "r"
-    val s:String = "s"
-    val t:String = "t"
-    val u:String = "u"
-    val v:String = "v"
-    val w:String = "w"
-    val x:String = "x"
-    val y:String = "y"
-    val z:String = "z"
-
-    case class SchematicFLabel(s:String){
-        def apply(ts:Term*): FunctionTerm = FunctionTerm(SchematicFunctionLabel(s, ts.length), ts)
-        def apply(n:Int): SchematicFunctionLabel = SchematicFunctionLabel(s, n)
-    }
-
-    case class SchematicPLabel(s:String){
-        def apply(fs:Term*): PredicateFormula = PredicateFormula(SchematicPredicateLabel(s, fs.length), fs)
-        def apply(n:Int): SchematicPredicateLabel = SchematicPredicateLabel(s, n)
-    }
-
-    //given Conversion[FunctionTerm, FunctionLabel] = _.label
-
-    def ?(s:String) = SchematicFLabel(s)
-    def &(s:String) = SchematicPLabel(s)
-
-    given Conversion[String, VariableLabel] = VariableLabel(_)
-    given Conversion[String, VariableTerm] = s => VariableTerm(VariableLabel(s))
-
-    ?("x")
-}

src/main/scala/proven/dev/MainLibrary.scala

-package proven.dev
-
-import lisa.kernel.proof.RunningTheory
-import lisa.settheory.AxiomaticSetTheory
-
-trait MainLibrary extends Library {
-  implicit val theory: RunningTheory = AxiomaticSetTheory.runningSetTheory
-  
-  import AxiomaticSetTheory.runningSetTheory.*
-
-}

src/main/scala/proven/dev/SetTheory.scala

-package proven.dev
-
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SCProof
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.settheory.AxiomaticSetTheory
-import lisa.settheory.AxiomaticSetTheory.*
-import proven.DSetTheory.Part1.{russelParadox, theory}
-import utilities.KernelHelpers.{*, given}
-import lisa.kernel.proof.RunningTheory
-
-trait SetTheory extends MainLibrary{
-  /*
-  private val x = SchematicFunctionLabel("x", 0)
-  private val y = SchematicFunctionLabel("y", 0)
-  private val z = SchematicFunctionLabel("z", 0)
-  private val x1 = VariableLabel("x")
-  private val y1 = VariableLabel("y")
-  private val z1 = VariableLabel("z")
-  private val f = SchematicFunctionLabel("f", 0)
-  private val g = SchematicFunctionLabel("g", 0)
-  private val h = SchematicPredicateLabel("h", 0)
-  */
-
-  private val `s?` = "sd"
-
-  given Conversion[SchematicFunctionLabel, Term] with
-    def apply(s: SchematicFunctionLabel): Term = s.apply()
-
-
-
-  val russelParadox: SCProof = {
-    val contra = (in(?y, ?y)) <=> !(in(?y, ?y))
-    val s0 = Hypothesis(contra |- contra, contra)
-    val s1 = LeftForall(forall(x, in(x, ?y) <=> !in(x, x)) |- contra, 0, in(x, ?y) <=> !in(x, x), x, ?y)
-    val s2 = Rewrite(forall(x, in(x, ?y) <=> !in(x, x)) |- (), 1)
-    SCProof(s0, s1, s2)
-  }
-  theorem("russelParadox", "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢", russelParadox, Nil).get
-
-}