diff --git a/Duper/Clause.lean b/Duper/Clause.lean
index 5fcf2ab..272eceb 100644
--- a/Duper/Clause.lean
+++ b/Duper/Clause.lean
@@ -51,8 +51,8 @@ def toExpr (lit : Lit) : Expr :=
 def fromSingleExpr (e : Expr) (sign := true) : Lit :=
   Lit.mk
     (sign := true)
-    (lvl := levelOne)
-    (ty := mkSort levelZero)
+    (lvl := Level.one)
+    (ty := mkSort Level.zero)
     (lhs := Expr.consumeMData e)
     (rhs := if sign then mkConst ``True else mkConst ``False)
 
diff --git a/Duper/Interface.lean b/Duper/Interface.lean
index d536851..3afcc4b 100644
--- a/Duper/Interface.lean
+++ b/Duper/Interface.lean
@@ -481,12 +481,16 @@ def formulasWithStringsToAutoLemmas (formulas : List (Expr × Expr × Array Name
 
 /-- Determines whether `lem`'s deriv info indicates that `lem` is part of the goal and should be included in the set of support. Note that `derivInfo`
     only works on lemmas generated from `formulasToAutoLemmas` or `formulasWithStringsToAutoLemmas`. In cases where the lemma was not generated from
-    `formulasToAutoLemmas`, `derivInfo` defaults to indicating that both `isFromGoal` and `includeInSetOfSupport` are `true`. -/
+    `formulasToAutoLemmas`, `derivInfo` defaults to indicating that both `isFromGoal` and `includeInSetOfSupport` are `true`. The only exception to this
+    is if all leaves have exactly the form "termLikeDefEq", in which case `derivInfo` indicates that `isFromGoal` is `false`. -/
 def derivInfo (lem : Auto.Lemma) : Bool × Bool :=
   let derivLeaves := getLeavesFromDTr lem.deriv
   let matchesFormat := derivLeaves.any (fun l => "true, true".isPrefixOf l || "false, true".isPrefixOf l || "true, false".isPrefixOf l || "false, false".isPrefixOf l)
   if !matchesFormat then
-    (true, true)
+    if derivLeaves.all (fun l => l == "termLikeDefEq") then
+      (false, true)
+    else
+      (true, true)
   else
     let isFromGoal := derivLeaves.any (fun l => "true".isPrefixOf l)
     let includeInSetOfSupport := derivLeaves.any (fun l => "true, true".isPrefixOf l || "false, true".isPrefixOf l)
diff --git a/Duper/Rules/BoolHoist.lean b/Duper/Rules/BoolHoist.lean
index 6fabf38..33ecddc 100644
--- a/Duper/Rules/BoolHoist.lean
+++ b/Duper/Rules/BoolHoist.lean
@@ -28,7 +28,7 @@ def boolHoistAtExpr (e : Expr) (pos : ClausePos) (given : Clause) (c : MClause)
       return #[]
     let eType ← inferType e
     let loaded ← getLoadedClauses
-    let ug ← unifierGenerator #[(eType, .sort levelZero)]
+    let ug ← unifierGenerator #[(eType, .sort Level.zero)]
     let yC := do
       setLoadedClauses loaded
       let lit := c.lits[pos.lit]!
diff --git a/Duper/Rules/BoolSimp.lean b/Duper/Rules/BoolSimp.lean
index 9c4a70f..da47564 100644
--- a/Duper/Rules/BoolSimp.lean
+++ b/Duper/Rules/BoolSimp.lean
@@ -320,7 +320,7 @@ partial def mkRule25Theorem (e : Expr) (counter : Nat) (i : Nat) (j : Nat) : Met
   | _ =>
     let iIdx := (counter - 1) - i
     let jIdx := (counter - 1) - j
-    return mkApp2 (mkConst ``False.elim [levelZero]) e (mkApp (Expr.bvar iIdx) (Expr.bvar jIdx))
+    return mkApp2 (mkConst ``False.elim [Level.zero]) e (mkApp (Expr.bvar iIdx) (Expr.bvar jIdx))
 
 /-- Assuming e has the form e1 ∨ e2 ∨ ... ∨ en, returns an array #[e1, e2, ... en].
     Note: If e has the form (e1a ∨ e1b) ∨ e2 ∨ ... en, then the disjunction (e1a ∨ e1b) will
@@ -870,7 +870,7 @@ partial def applyRule27 (e : Expr) : RuleM (Option (Nat × Nat)) := do
 /-- s1 ↔ s2 ↦ s1 = s2 -/
 def applyRule28 (e : Expr) : Option Expr :=
   match e with
-  | Expr.app (Expr.app (Expr.const ``Iff _) e1) e2 => some $ mkApp3 (mkConst ``Eq [levelOne]) (mkSort levelZero) e1 e2
+  | Expr.app (Expr.app (Expr.const ``Iff _) e1) e2 => some $ mkApp3 (mkConst ``Eq [Level.one]) (mkSort Level.zero) e1 e2
   | _ => none
 
 /-- Returns the rule theorem corresponding to boolSimpRule with the first argument applied.
@@ -1095,7 +1095,7 @@ def getBoolSimpRuleTheorem (boolSimpRule : BoolSimpRule) (originalExp : Expr) (i
   | rule23 => -- ∀ p : Prop, f(p) ↦ f(True) ∧ f(False)
     match originalExp.consumeMData with
     | Expr.forallE n _ b _ => do
-      let bFunction := Expr.lam n (mkSort levelZero) b BinderInfo.default
+      let bFunction := Expr.lam n (mkSort Level.zero) b BinderInfo.default
       return mkApp (mkConst ``rule23Theorem) bFunction
     | _ => throwError "Invalid originalExp {originalExp} for rule23"
   | rule23b => -- ∀ b : Bool, f(b) ↦ f true ∧ f false (assuming `f : Bool → Prop`)
@@ -1157,7 +1157,7 @@ def mkBoolSimpProof (substPos : ClausePos) (boolSimpRule : BoolSimpRule) (ijOpt
           let abstrExp := abstrLit.toExpr
           let abstrLam :=
             if boolSimpRuleOperatesOnBool boolSimpRule then mkLambda `x BinderInfo.default (mkConst ``Bool) abstrExp
-            else mkLambda `x BinderInfo.default (mkSort levelZero) abstrExp
+            else mkLambda `x BinderInfo.default (mkSort Level.zero) abstrExp
           let rwproof ← Meta.mkAppM ``Eq.mp #[← Meta.mkAppM ``congrArg #[abstrLam, boolSimpRuleThm], h]
           Meta.mkLambdaFVars #[h] $ ← orIntro (cLits.map Lit.toExpr) i $ rwproof
         else
diff --git a/Duper/Rules/ContextualLiteralCutting.lean b/Duper/Rules/ContextualLiteralCutting.lean
index 5bda581..8abc3a1 100644
--- a/Duper/Rules/ContextualLiteralCutting.lean
+++ b/Duper/Rules/ContextualLiteralCutting.lean
@@ -49,7 +49,7 @@ def mkContextualLiteralCuttingProof (negatedLitMainIdx : Nat) (assignment : List
                       let hSideFlipped ← Meta.mkAppM ``Eq.symm #[hSide]
                       Meta.mkAppM' hMain #[hSideFlipped]
                     else Meta.mkAppM' hMain #[hSide]
-                Meta.mkLambdaFVars #[hMain] $ mkApp2 (mkConst ``False.elim [levelZero]) body contraProof
+                Meta.mkLambdaFVars #[hMain] $ mkApp2 (mkConst ``False.elim [Level.zero]) body contraProof
               caseProofsMain := caseProofsMain.push pr
             else
               let pr ← Meta.withLocalDeclD `hMain curMainLit.toExpr fun hMain => do
diff --git a/Duper/Rules/DatatypeAcyclicity.lean b/Duper/Rules/DatatypeAcyclicity.lean
index 73e0d24..76be706 100644
--- a/Duper/Rules/DatatypeAcyclicity.lean
+++ b/Duper/Rules/DatatypeAcyclicity.lean
@@ -167,7 +167,7 @@ def mkDatatypeAcyclicityProof (removedLitNum : Nat) (litSide : LitSide) (premise
           let gtProof ← buildGtProof lit.lhs lit.rhs
           let neProof ← mkAppM ``Nat.ne_of_gt #[gtProof]
           sizeOfEqFalseMVarId.assign neProof
-          let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body $ mkApp sizeOfEqFalseMVar sizeOfEq -- Has the type `body`
+          let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body $ mkApp sizeOfEqFalseMVar sizeOfEq -- Has the type `body`
           trace[duper.rule.datatypeAcyclicity] "lit: {lit}, lit.ty: {lit.ty}, sizeOfInst: {sizeOfInst}, abstrLam: {abstrLam}, sizeOfEq: {sizeOfEq}"
           trace[duper.rule.datatypeAcyclicity] "sizeOfEqFalseMVar: {sizeOfEqFalseMVar}, proofCase: {proofCase}"
           Meta.mkLambdaFVars #[h] proofCase
diff --git a/Duper/Rules/DatatypeDistinctness.lean b/Duper/Rules/DatatypeDistinctness.lean
index fcca11f..f2e354e 100644
--- a/Duper/Rules/DatatypeDistinctness.lean
+++ b/Duper/Rules/DatatypeDistinctness.lean
@@ -74,7 +74,7 @@ def mkDatatypeDistinctnessProof (refs : List (Option Nat)) (premises : List Expr
               pure $ #[some (mkConst ``False)] ++ (Array.range (2 * numParams + 2)).map (fun _ => none) ++
                 (← (Array.range numParams).mapM (fun x => do pure $ some (← mkAppOptM ``rfl #[none, some (lit.ty.getAppArgs[x]!)]))) ++ #[some (← mkAppM ``heq_of_eq #[h])]
           let proofCase ← mkAppOptM' (mkConst (.str tyName "noConfusion") (0 :: lvls)) noConfusionArgs
-          let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+          let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
           Meta.mkLambdaFVars #[h] proofCase
         proofCases := proofCases.push proofCase
       | none => -- refs[i] should have the value (some j) where parentLits[i] == c[j]
diff --git a/Duper/Rules/DatatypeInjectivity.lean b/Duper/Rules/DatatypeInjectivity.lean
index b056fa9..b9733d4 100644
--- a/Duper/Rules/DatatypeInjectivity.lean
+++ b/Duper/Rules/DatatypeInjectivity.lean
@@ -97,7 +97,7 @@ def mkDatatypeInjectivityNegProof (removedLitNum : Nat) (premises : List Expr) (
             match ← inferType injEq with
             | Expr.app (Expr.app (Expr.app (Expr.const ``Eq [_]) _) _) e2 => pure e2
             | _ => throwError "mkDatatypeInjectivityNegProof :: Type of {injEq} is not an equality as expected"
-          let propMVar ← mkFreshExprMVar (mkSort levelZero)
+          let propMVar ← mkFreshExprMVar (mkSort Level.zero)
           let abstrLam ← mkLambdaFVars #[propMVar] $ ← mkAppM ``Eq #[← mkAppM ``Not #[propMVar], ← mkAppM ``Not #[argEqualities]]
           let proofCase ← mkAppM ``Eq.mpr #[← mkAppM ``congrArg #[abstrLam, injEq], ← mkAppM ``Eq.refl #[← mkAppM ``Not #[argEqualities]]]
           let proofCase ← mkAppM ``Eq.mp #[proofCase, h]
diff --git a/Duper/Rules/DecElim.lean b/Duper/Rules/DecElim.lean
index 216bae4..aeadef5 100644
--- a/Duper/Rules/DecElim.lean
+++ b/Duper/Rules/DecElim.lean
@@ -52,7 +52,7 @@ def mkDecElimProof (refs : List (Option Nat)) (premises : List Expr) (parents :
         trace[duper.rule.decElim] "Built {proofCase} proving {d} is false"
         let pr ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           let proofCase := mkApp proofCase h
-          let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+          let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
           Meta.mkLambdaFVars #[h] proofCase
         caseProofs := caseProofs.push pr
       | some j =>
diff --git a/Duper/Rules/DestructiveEqualityResolution.lean b/Duper/Rules/DestructiveEqualityResolution.lean
index cab23ba..9ed666d 100644
--- a/Duper/Rules/DestructiveEqualityResolution.lean
+++ b/Duper/Rules/DestructiveEqualityResolution.lean
@@ -32,7 +32,7 @@ def mkDestructiveEqualtiyResolutionProof (i : Nat) (premises : List Expr) (paren
         let pr ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           let pr := mkApp2 (mkConst ``rfl [lit.lvl]) lit.ty lit.lhs
           let pr := mkApp h pr
-          let pr := mkApp2 (mkConst ``False.elim [levelZero]) body pr
+          let pr := mkApp2 (mkConst ``False.elim [Level.zero]) body pr
           Meta.mkLambdaFVars #[h] pr
         caseProofs := caseProofs.push pr
       else
diff --git a/Duper/Rules/ElimResolvedLit.lean b/Duper/Rules/ElimResolvedLit.lean
index be29d04..6e5903b 100644
--- a/Duper/Rules/ElimResolvedLit.lean
+++ b/Duper/Rules/ElimResolvedLit.lean
@@ -28,7 +28,7 @@ def mkElimResolvedLitProof (refs : List (Option Nat)) (premises : List Expr) (pa
         let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           let proofCase := mkApp2 (mkConst ``rfl [lit.lvl]) lit.ty lit.lhs
           let proofCase := mkApp h proofCase
-          let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+          let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
           Meta.mkLambdaFVars #[h] proofCase
         proofCases := proofCases.push proofCase
       else
diff --git a/Duper/Rules/EqHoist.lean b/Duper/Rules/EqHoist.lean
index 7e5163a..2fc6cc6 100644
--- a/Duper/Rules/EqHoist.lean
+++ b/Duper/Rules/EqHoist.lean
@@ -39,7 +39,7 @@ def mkEqHoistProof (pos : ClausePos) (premises : List Expr)
           let substLitPos : LitPos := ⟨pos.side, pos.pos⟩
           let abstrLit ← (lit.abstractAtPos! substLitPos)
           let abstrExp := abstrLit.toExpr
-          let abstrLam := mkLambda `x BinderInfo.default (mkSort levelZero) abstrExp
+          let abstrLam := mkLambda `x BinderInfo.default (mkSort Level.zero) abstrExp
           let lastTwoClausesProof ← Meta.mkAppM ``eq_hoist_proof #[freshVar1, freshVar2, abstrLam, h]
           Meta.mkLambdaFVars #[h] $ ← orSubclause (cLits.map Lit.toExpr) 2 lastTwoClausesProof
         else
diff --git a/Duper/Rules/EqualityResolution.lean b/Duper/Rules/EqualityResolution.lean
index e7d95e6..808b2fd 100644
--- a/Duper/Rules/EqualityResolution.lean
+++ b/Duper/Rules/EqualityResolution.lean
@@ -27,7 +27,7 @@ def mkEqualityResolutionProof (i : Nat) (premises : List Expr) (parents : List P
         let pr ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           let pr := mkApp2 (mkConst ``rfl [lit.lvl]) lit.ty lit.lhs
           let pr := mkApp h pr
-          let pr := mkApp2 (mkConst ``False.elim [levelZero]) body pr
+          let pr := mkApp2 (mkConst ``False.elim [Level.zero]) body pr
           Meta.mkLambdaFVars #[h] pr
         caseProofs := caseProofs.push pr
       else
diff --git a/Duper/Rules/ExistsHoist.lean b/Duper/Rules/ExistsHoist.lean
index 7c27b59..c499f81 100644
--- a/Duper/Rules/ExistsHoist.lean
+++ b/Duper/Rules/ExistsHoist.lean
@@ -38,7 +38,7 @@ def mkExistsHoistProof (pos : ClausePos) (premises : List Expr) (parents : List
           let substLitPos : LitPos := ⟨pos.side, pos.pos⟩
           let abstrLit ← (lit.abstractAtPos! substLitPos)
           let abstrExp := abstrLit.toExpr
-          let abstrLam := mkLambda `x BinderInfo.default (mkSort levelZero) abstrExp
+          let abstrLam := mkLambda `x BinderInfo.default (mkSort Level.zero) abstrExp
           let lastTwoLitsProof ← Meta.mkAppM ``exists_hoist_proof #[freshVar1, abstrLam, h]
           Meta.mkLambdaFVars #[h] $ ← orSubclause (cLits.map Lit.toExpr) 2 lastTwoLitsProof
         else
@@ -70,7 +70,7 @@ def existsHoistAtExpr (e : Expr) (pos : ClausePos) (given : Clause) (c : MClause
     -- Make freshVars, freshVarExistsExpr and newLitLhs
     let freshVar1 ← mkFreshExprMVar none
     let freshVar1Ty ← inferType freshVar1
-    let freshVar2Ty := Expr.forallE .anonymous freshVar1Ty (mkSort levelZero) BinderInfo.default -- freshVar1Ty → Prop
+    let freshVar2Ty := Expr.forallE .anonymous freshVar1Ty (mkSort Level.zero) BinderInfo.default -- freshVar1Ty → Prop
     let freshVar2 ← mkFreshExprMVar freshVar2Ty
     let freshVarExistsExpr ← mkAppM ``Exists #[freshVar2]
     let newLitLhs := .app freshVar2 freshVar1
diff --git a/Duper/Rules/FalseElim.lean b/Duper/Rules/FalseElim.lean
index e2f19f0..cc536d0 100644
--- a/Duper/Rules/FalseElim.lean
+++ b/Duper/Rules/FalseElim.lean
@@ -38,13 +38,13 @@ def mkFalseElimProof (i : Nat) (premises : List Expr) (parents : List ProofParen
         if lit.lhs == mkConst ``True then -- lit unified with `True = False`
           let pr ← Meta.withLocalDeclD `h lit.toExpr fun h => do
             let proofCase := mkApp (mkConst ``true_ne_false) h
-            let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+            let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
             Meta.mkLambdaFVars #[h] proofCase
           caseProofs := caseProofs.push pr
         else -- lit unified with `False = True`
           let pr ← Meta.withLocalDeclD `h lit.toExpr fun h => do
             let proofCase := mkApp (mkConst ``false_ne_true) h
-            let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+            let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
             Meta.mkLambdaFVars #[h] proofCase
           caseProofs := caseProofs.push pr
       else
diff --git a/Duper/Rules/FluidBoolHoist.lean b/Duper/Rules/FluidBoolHoist.lean
index 8d39684..adc5063 100644
--- a/Duper/Rules/FluidBoolHoist.lean
+++ b/Duper/Rules/FluidBoolHoist.lean
@@ -77,8 +77,8 @@ def fluidBoolHoistAtExpr (e : Expr) (pos : ClausePos) (given : Clause) (c : MCla
     if litEligibility == Eligibility.notEligible || sideComparison == Comparison.LessThan then return #[]
 
     let freshFunctionOutputType ← inferType e
-    let freshFunction ← mkFreshFunction (mkSort levelZero) freshFunctionOutputType -- mkFreshFunction defined in FluidSup.lean
-    let freshPropVar ← mkFreshExprMVar (mkSort levelZero)
+    let freshFunction ← mkFreshFunction (mkSort Level.zero) freshFunctionOutputType -- mkFreshFunction defined in FluidSup.lean
+    let freshPropVar ← mkFreshExprMVar (mkSort Level.zero)
     let freshFunctionApp ← Meta.whnf (.app freshFunction freshPropVar)
 
     let loaded ← getLoadedClauses
diff --git a/Duper/Rules/ForallHoist.lean b/Duper/Rules/ForallHoist.lean
index 98f1815..f2763fe 100644
--- a/Duper/Rules/ForallHoist.lean
+++ b/Duper/Rules/ForallHoist.lean
@@ -38,7 +38,7 @@ def mkForallHoistProof (pos : ClausePos) (premises : List Expr)
           let substLitPos : LitPos := ⟨pos.side, pos.pos⟩
           let abstrLit ← (lit.abstractAtPos! substLitPos)
           let abstrExp := abstrLit.toExpr
-          let abstrLam := mkLambda `x BinderInfo.default (mkSort levelZero) abstrExp
+          let abstrLam := mkLambda `x BinderInfo.default (mkSort Level.zero) abstrExp
           let lastTwoLitsProof ← Meta.mkAppM ``forall_hoist_proof #[freshVar1, abstrLam, h]
           Meta.mkLambdaFVars #[h] $ ← orSubclause (cLits.map Lit.toExpr) 2 lastTwoLitsProof
         else
@@ -51,7 +51,7 @@ def mkForallHoistProof (pos : ClausePos) (premises : List Expr)
 /-- Returns the dependent forall and lambda expressions -/
 def mkForallAndLambda (freshVar1Ty : Expr) : MetaM (Expr × Expr) :=
   Meta.withLocalDeclD `_ freshVar1Ty fun fvar => do
-    let newMVar ← Meta.mkFreshExprMVar (mkSort levelZero)
+    let newMVar ← Meta.mkFreshExprMVar (mkSort Level.zero)
     let forallExpr ← Meta.mkForallFVars #[fvar] newMVar
     let lambdaExpr ← Meta.mkLambdaFVars #[fvar] newMVar
     return (forallExpr, lambdaExpr)
diff --git a/Duper/Rules/IdentBoolFalseElim.lean b/Duper/Rules/IdentBoolFalseElim.lean
index 4b2c1f4..26388ce 100644
--- a/Duper/Rules/IdentBoolFalseElim.lean
+++ b/Duper/Rules/IdentBoolFalseElim.lean
@@ -36,11 +36,11 @@ def mkIdentBoolFalseElimProof (refs : List (Option Nat)) (premises : List Expr)
         let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           if (lit.lhs == mkConst ``false) then
             let proofCase := mkApp (mkConst ``bool_false_ne_true) h
-            let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+            let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
             Meta.mkLambdaFVars #[h] proofCase
           else if(lit.lhs == mkConst ``true) then
             let proofCase := mkApp (mkConst ``bool_true_ne_false) h
-            let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+            let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
             Meta.mkLambdaFVars #[h] proofCase
           else
             throwError "mkIdentBoolFalseElimProof failed to match {lit.lhs} to an expected expression"
diff --git a/Duper/Rules/IdentPropFalseElim.lean b/Duper/Rules/IdentPropFalseElim.lean
index 6696a74..e98b94e 100644
--- a/Duper/Rules/IdentPropFalseElim.lean
+++ b/Duper/Rules/IdentPropFalseElim.lean
@@ -16,7 +16,7 @@ initialize Lean.registerTraceClass `duper.rule.identPropFalseElim
 def isFalsePropLiteral (lit : Lit) : MetaM Bool := do
   match lit.ty with
   | Expr.sort lvl =>
-    if Level.isEquiv (← Lean.instantiateLevelMVars lvl) levelZero then
+    if Level.isEquiv (← Lean.instantiateLevelMVars lvl) Level.zero then
       return lit.sign &&
         ((lit.lhs == mkConst ``True && lit.rhs == mkConst ``False) ||
         (lit.lhs == mkConst ``False && lit.rhs == mkConst ``True))
@@ -42,11 +42,11 @@ def mkIdentPropFalseElimProof (refs : List (Option Nat)) (premises : List Expr)
         let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           if (lit.lhs == mkConst ``False) then
             let proofCase := mkApp (mkConst ``prop_false_ne_true) h
-            let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+            let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
             Meta.mkLambdaFVars #[h] proofCase
           else if(lit.lhs == mkConst ``True) then
             let proofCase := mkApp (mkConst ``prop_true_ne_false) h
-            let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+            let proofCase := mkApp2 (mkConst ``False.elim [Level.zero]) body proofCase
             Meta.mkLambdaFVars #[h] proofCase
           else
             throwError "mkIdentPropFalseElimProof failed to match {lit.lhs} to an expected expression"
diff --git a/Duper/Rules/NeHoist.lean b/Duper/Rules/NeHoist.lean
index 81b7014..a0af35d 100644
--- a/Duper/Rules/NeHoist.lean
+++ b/Duper/Rules/NeHoist.lean
@@ -39,7 +39,7 @@ def mkNeHoistProof (pos : ClausePos) (premises : List Expr)
           let substLitPos : LitPos := ⟨pos.side, pos.pos⟩
           let abstrLit ← (lit.abstractAtPos! substLitPos)
           let abstrExp := abstrLit.toExpr
-          let abstrLam := mkLambda `x BinderInfo.default (mkSort levelZero) abstrExp
+          let abstrLam := mkLambda `x BinderInfo.default (mkSort Level.zero) abstrExp
           let lastTwoClausesProof ← Meta.mkAppM ``ne_hoist_proof #[freshVar1, freshVar2, abstrLam, h]
           Meta.mkLambdaFVars #[h] $ ← orSubclause (cLits.map Lit.toExpr) 2 lastTwoClausesProof
         else
diff --git a/Duper/Rules/SimplifyReflect.lean b/Duper/Rules/SimplifyReflect.lean
index c1e3542..3a79a08 100644
--- a/Duper/Rules/SimplifyReflect.lean
+++ b/Duper/Rules/SimplifyReflect.lean
@@ -38,13 +38,13 @@ def mkPositiveSimplifyReflectProof (mainPremisePos : ClausePos) (isForward : Boo
                 mkLambda .anonymous BinderInfo.default motiveTy $
                   mkAppN (mkConst ``Ne [lit.lvl]) #[lit.ty, ← lit.lhs.replaceAtPos! mainPremisePos.pos (Expr.bvar 0), lit.rhs]
               let hAfterRw ← Meta.mkAppOptM ``Eq.ndrec #[none, none, motive, h, none, appliedSidePremise]
-              Meta.mkLambdaFVars #[h] $ mkApp2 (mkConst ``False.elim [levelZero]) body $ ← Meta.mkAppM' hAfterRw #[← Meta.mkAppM ``Eq.refl #[lit.rhs]]
+              Meta.mkLambdaFVars #[h] $ mkApp2 (mkConst ``False.elim [Level.zero]) body $ ← Meta.mkAppM' hAfterRw #[← Meta.mkAppM ``Eq.refl #[lit.rhs]]
             else -- the lhs of the side clause can be matched onto mainPremisePos.pos of lit.rhs
               let motive :=
                 mkLambda .anonymous BinderInfo.default motiveTy $
                   mkAppN (mkConst ``Ne [lit.lvl]) #[lit.ty, lit.lhs, ← lit.rhs.replaceAtPos! mainPremisePos.pos (Expr.bvar 0)]
               let hAfterRw ← Meta.mkAppOptM ``Eq.ndrec #[none, none, motive, h, none, appliedSidePremise]
-              Meta.mkLambdaFVars #[h] $ mkApp2 (mkConst ``False.elim [levelZero]) body $ ← Meta.mkAppM' hAfterRw #[← Meta.mkAppM ``Eq.refl #[lit.lhs]]
+              Meta.mkLambdaFVars #[h] $ mkApp2 (mkConst ``False.elim [Level.zero]) body $ ← Meta.mkAppM' hAfterRw #[← Meta.mkAppM ``Eq.refl #[lit.lhs]]
           else if (i < mainPremisePos.lit) then
             Meta.mkLambdaFVars #[h] $ ← orIntro (cLits.map Lit.toExpr) i h
           else -- i > mainPremisePos.lit, so we have to adjust for the off-by-one error by giving orIntro `i - 1` rather than `i`
@@ -75,9 +75,9 @@ def mkNegativeSimplifyReflectProof (mainPremiseLitIdx : Nat) (mainPremiseLhs : L
         let pr : Expr ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           if(i == mainPremiseLitIdx) then
             if mainPremiseLhs == LitSide.lhs then
-              Meta.mkLambdaFVars #[h] $ mkApp2 (mkConst ``False.elim [levelZero]) body $ mkApp appliedSidePremise h
+              Meta.mkLambdaFVars #[h] $ mkApp2 (mkConst ``False.elim [Level.zero]) body $ mkApp appliedSidePremise h
             else
-              Meta.mkLambdaFVars #[h] $ mkApp2 (mkConst ``False.elim [levelZero]) body $ mkApp (← Meta.mkAppM ``Ne.symm #[appliedSidePremise]) h
+              Meta.mkLambdaFVars #[h] $ mkApp2 (mkConst ``False.elim [Level.zero]) body $ mkApp (← Meta.mkAppM ``Ne.symm #[appliedSidePremise]) h
           else if (i < mainPremiseLitIdx) then
             Meta.mkLambdaFVars #[h] $ ← orIntro (cLits.map Lit.toExpr) i h
           else -- i > mainPremisePos.lit, so we have to adjust for the off-by-one error by giving orIntro `i - 1` rather than `i`
diff --git a/Duper/TPTPParser/PrattParser.lean b/Duper/TPTPParser/PrattParser.lean
index 332ebc8..d7914fe 100644
--- a/Duper/TPTPParser/PrattParser.lean
+++ b/Duper/TPTPParser/PrattParser.lean
@@ -345,8 +345,8 @@ open Meta
 partial def toLeanExpr (t : Parser.Term) : MetaM Expr := do
   match t with
   | ⟨.ident "$i", []⟩ => return mkConst `Iota
-  | ⟨.ident "$tType", []⟩ => return mkSort levelOne
-  | ⟨.ident "$o", []⟩ => return mkSort levelZero
+  | ⟨.ident "$tType", []⟩ => return mkSort Level.one
+  | ⟨.ident "$o", []⟩ => return mkSort Level.zero
   | ⟨.ident "$true", []⟩ => return mkConst `True
   | ⟨.ident "$false", []⟩ => return mkConst `False
   | ⟨.ident n, as⟩ => do
@@ -386,20 +386,20 @@ partial def toLeanExpr (t : Parser.Term) : MetaM Expr := do
   | ⟨.op "<=>", []⟩ => pure $ mkConst `Iff
   | ⟨.op "!=", []⟩  => pure $ mkConst `Ne
   | ⟨.op "=", []⟩   => pure $ mkConst `Eq
-  | ⟨.op "~|", []⟩  => pure $ mkLambda `x .default (mkSort levelZero) $
-                         mkLambda `y .default (mkSort levelZero) $
+  | ⟨.op "~|", []⟩  => pure $ mkLambda `x .default (mkSort Level.zero) $
+                         mkLambda `y .default (mkSort Level.zero) $
                            mkAppN (mkConst ``Not) #[mkAppN (mkConst ``Or) #[.bvar 1, .bvar 0]]
-  | ⟨.op "~&", []⟩  => pure $ mkLambda `x .default (mkSort levelZero) $
-                         mkLambda `y .default (mkSort levelZero) $
+  | ⟨.op "~&", []⟩  => pure $ mkLambda `x .default (mkSort Level.zero) $
+                         mkLambda `y .default (mkSort Level.zero) $
                            mkAppN (mkConst ``Not) #[mkAppN (mkConst ``And) #[.bvar 1, .bvar 0]]
-  | ⟨.op "<~>", []⟩  => pure $ mkLambda `x .default (mkSort levelZero) $
-                         mkLambda `y .default (mkSort levelZero) $
+  | ⟨.op "<~>", []⟩  => pure $ mkLambda `x .default (mkSort Level.zero) $
+                         mkLambda `y .default (mkSort Level.zero) $
                            mkAppN (mkConst ``Not) #[mkAppN (mkConst ``Iff) #[.bvar 1, .bvar 0]]
-  | ⟨.op "=>", []⟩  => pure $ mkLambda `x .default (mkSort levelZero) $
-                         mkLambda `y .default (mkSort levelZero) $
+  | ⟨.op "=>", []⟩  => pure $ mkLambda `x .default (mkSort Level.zero) $
+                         mkLambda `y .default (mkSort Level.zero) $
                            Lean.mkForall `i BinderInfo.default (.bvar 1) (.bvar 1)
-  | ⟨.op "<=", []⟩  => pure $ mkLambda `x .default (mkSort levelZero) $
-                         mkLambda `y .default (mkSort levelZero) $
+  | ⟨.op "<=", []⟩  => pure $ mkLambda `x .default (mkSort Level.zero) $
+                         mkLambda `y .default (mkSort Level.zero) $
                            Lean.mkForall `i BinderInfo.default (.bvar 0) (.bvar 2)
 
   | ⟨.op ">", [⟨.op "*", [a, b]⟩, c]⟩   => toLeanExpr ⟨.op ">", [a, ⟨.op ">", [b, c]⟩]⟩
@@ -497,7 +497,7 @@ partial def collectConstantsOfCmd (topLevel : Bool) (acc : Std.HashMap String Ex
     then
       let ty ← as.foldlM
         (fun acc _ => mkArrow (mkConst `Iota) acc)
-        (if topLevel then mkSort levelZero else mkConst `Iota)
+        (if topLevel then mkSort Level.zero else mkConst `Iota)
       let acc := acc.insert n ty
       return acc
     else
diff --git a/Main.lean b/Main.lean
index 9c0c15a..73362ab 100644
--- a/Main.lean
+++ b/Main.lean
@@ -36,8 +36,8 @@ def runDuperOnTPTP (fileName : String) (formulas : List (Expr × Expr × Array N
   | Result.unknown => IO.println s!"SZS status Timeout for {fileName}"
 
 def run (path : String) (_github : Bool) : MetaM Unit := do
-  let prop := mkSort levelZero
-  let type := mkSort levelOne
+  let prop := mkSort Level.zero
+  let type := mkSort Level.one
   let sortu := mkSort (.param `u)
   let sortu1 := mkSort (.param `u1)
   let sortu2 := mkSort (.param `u2)
@@ -73,13 +73,13 @@ def run (path : String) (_github : Bool) : MetaM Unit := do
       type :=
         mkForall `p .implicit prop $
         mkForall `h .default (.bvar 0) $
-        (mkApp3 (mkConst ``Eq [levelOne]) prop (.bvar 1) (mkConst ``True [])),
+        (mkApp3 (mkConst ``Eq [Level.one]) prop (.bvar 1) (mkConst ``True [])),
       isUnsafe := false})
   addDecl (.axiomDecl
     { name := `of_eq_true, levelParams := [],
       type :=
         mkForall `p .implicit prop $
-        mkForall `h .default (mkApp3 (mkConst ``Eq [levelOne]) prop (.bvar 0) (mkConst ``True [])) $
+        mkForall `h .default (mkApp3 (mkConst ``Eq [Level.one]) prop (.bvar 0) (mkConst ``True [])) $
         (.bvar 1),
       isUnsafe := false})
 
diff --git a/lake-manifest.json b/lake-manifest.json
index ac03469..2b050f9 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,25 +1,26 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
+   "rev": "32dc18cde3684679f3c003de608743b57498c56f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.30.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d5600411d5e766a7cb1e47e3b3393ed64c42efc2",
+   "rev": "2f8e2034b14834cf2577d7f400bd8fe32ab7179f",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0-hammer",
+   "inputRev": "v4.30.0-hammer",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Duper",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.lean b/lakefile.lean
index 8aa415e..97e85dc 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v4.29.0-hammer"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.29.0"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v4.30.0-hammer"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.30.0"
 
 package Duper {
   precompileModules := true
diff --git a/lean-toolchain b/lean-toolchain
index 14791d7..5a8f161 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.30.0
\ No newline at end of file