diff --git a/Auto/Embedding/LamBase.lean b/Auto/Embedding/LamBase.lean
index d88390e..6da9948 100644
--- a/Auto/Embedding/LamBase.lean
+++ b/Auto/Embedding/LamBase.lean
@@ -3935,17 +3935,17 @@ def LamWF.ofLamCheck? {ltv : LamTyVal} :
       rw [LamSort.eq_of_beq_eq_true h₂] at h₁
       apply LamWF.ofLamCheck? h₁
 
-noncomputable def LamWF.interp.{u} (lval : LamValuation.{u}) :
-  (lctxTy : Nat → LamSort) → (lctxTerm : ∀ n, (lctxTy n).interp lval.tyVal) →
+noncomputable def LamWF.interp.{u} (lval : LamValuation.{u})
+  (lctxTy : Nat → LamSort) (lctxTerm : ∀ n, (lctxTy n).interp lval.tyVal) :
   (lwf : LamWF lval.toLamTyVal ⟨lctxTy, t, rty⟩) → rty.interp lval.tyVal
-| _,      _       , .ofAtom n => lval.varVal n
-| _,      _       , .ofEtom n => lval.eVarVal n
-| _,      _       , .ofBase H => LamBaseTerm.LamWF.interp lval H
-| lctxTy, lctxTerm, .ofBVar n => lctxTerm n
-| lctxTy, lctxTerm, @LamWF.ofLam _ _ argTy _ body H =>
+| .ofAtom n => lval.varVal n
+| .ofEtom n => lval.eVarVal n
+| .ofBase H => LamBaseTerm.LamWF.interp lval H
+| .ofBVar n => lctxTerm n
+| @ofLam _ _ argTy _ body H =>
   fun (x : argTy.interp lval.tyVal) =>
     LamWF.interp lval (pushLCtx argTy lctxTy) (pushLCtxDep (rty:=lctxTy) x lctxTerm) H
-| lctxTy, lctxTerm, .ofApp _ HFn HArg =>
+| .ofApp _ HFn HArg =>
   let mfn := LamWF.interp lval lctxTy lctxTerm HFn
   let marg := LamWF.interp lval lctxTy lctxTerm HArg
   mfn marg
diff --git a/Auto/Lib/BinTree.lean b/Auto/Lib/BinTree.lean
index c5f4e57..f208940 100644
--- a/Auto/Lib/BinTree.lean
+++ b/Auto/Lib/BinTree.lean
@@ -20,12 +20,9 @@ open ToExprExtra
 
 namespace Bin
 
-private theorem wfAux (n n' : Nat) : n = n' + 2 → n / 2 < n := by
-  intro H; apply Nat.div_lt_self
-  case hLtN =>
-    cases n;
-    contradiction;
-    apply Nat.succ_le_succ; apply Nat.zero_le
+private theorem wfAux (n : Nat) : (n + 2).div 2 < n + 2 := by
+  apply Nat.div_lt_self
+  case hLtN => apply Nat.succ_le_succ; apply Nat.zero_le
   case hLtK => apply Nat.le_refl
 
 def inductionOn.{u}
@@ -36,7 +33,6 @@ def inductionOn.{u}
   | 0 => base₀
   | 1 => base₁
   | x' + 2 => ind x' (inductionOn ((x' + 2) / 2) ind base₀ base₁)
-decreasing_by apply wfAux; rfl
 
 @[irreducible] def induction.{u}
   {motive : Nat → Sort u}
@@ -118,16 +114,16 @@ def right! (bt : BinTree α) :=
   | .leaf => leaf
   | .node _ _ r => r
 
+attribute [local simp] Bin.wfAux
+
 def get?'WF (bt : BinTree α) (n : Nat) : Option α :=
-  match h : n with
+  match _ : n with
   | 0 => .none
   | 1 => bt.val?
   | _ + 2 =>
     match Nat.mod n 2 with
     | 0 => get?'WF bt.left! (Nat.div n 2)
     | _ + 1 => get?'WF bt.right! (Nat.div n 2)
-termination_by n
-decreasing_by all_goals { rw [← h]; apply Bin.wfAux; assumption }
 
 theorem get?'WF.succSucc (bt : BinTree α) (n : Nat) :
   get?'WF bt (n + 2) =
@@ -200,7 +196,7 @@ theorem get?'_leaf (n : Nat) : @get?' α .leaf n = .none := by
     cases (n + 2) % 2 <;> exact IH
 
 def insert'WF (bt : BinTree α) (n : Nat) (x : α) : BinTree α :=
-  match h : n with
+  match _ : n with
   | 0 => bt
   | 1 =>
     match bt with
@@ -216,8 +212,6 @@ def insert'WF (bt : BinTree α) (n : Nat) (x : α) : BinTree α :=
       match bt with
       | .leaf => .node .leaf .none (insert'WF .leaf (Nat.div n 2) x)
       | .node l v r => .node l v (insert'WF r (Nat.div n 2) x)
-termination_by n
-decreasing_by all_goals { rw [← h]; apply Bin.wfAux; assumption }
 
 theorem insert'WF.succSucc (bt : BinTree α) (n : Nat) (x : α) :
   insert'WF bt (n + 2) x =
diff --git a/Auto/Lib/Pos.lean b/Auto/Lib/Pos.lean
index 2fdfec9..c4bed8e 100644
--- a/Auto/Lib/Pos.lean
+++ b/Auto/Lib/Pos.lean
@@ -40,14 +40,13 @@ private theorem ofNat'WFAux (n n' : Nat) : n = n' + 2 → n / 2 < n := by
   case hLtK => apply Nat.le_refl
 
 def ofNat'WF (n : Nat) :=
-  match h : n with
+  match _ : n with
   | 0 => xH
   | 1 => xH
   | _ + 2 =>
     match n % 2 with
     | 0 => .xO (ofNat'WF (n / 2))
     | _ => .xI (ofNat'WF (n / 2))
-decreasing_by rw [h]; apply ofNat'WFAux _ _ rfl
 
 def ofNat'WF.inductionOn.{u}
   {motive : Nat → Sort u} (x : Nat)
diff --git a/Auto/Translation/Reduction.lean b/Auto/Translation/Reduction.lean
index 2707a46..a8a5096 100644
--- a/Auto/Translation/Reduction.lean
+++ b/Auto/Translation/Reduction.lean
@@ -9,6 +9,7 @@ private instance : ToString TransparencyMode where
   | .default   => "default"
   | .reducible => "reducible"
   | .instances => "instances"
+  | .none      => "none"
 
 private instance : Lean.KVMap.Value TransparencyMode where
   toDataValue t := toString t
@@ -17,6 +18,7 @@ private instance : Lean.KVMap.Value TransparencyMode where
   | "default"   => some .default
   | "reducible" => some .reducible
   | "instances" => some .instances
+  | "none"      => some .none
   | _           => none
 
 register_option auto.redMode : TransparencyMode := {
diff --git a/lean-toolchain b/lean-toolchain
index 5249182..4c685fa 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.28.0