refactor: migrate to the new do elaborator

Lean4Lean/EquivManager.lean

@@ -1,15 +1,6 @@
 import Batteries.Data.UnionFind.Basic
 import Lean4Lean.PtrEq
 
-/-
-The `Lean4Lean.Verify` proofs about the definitions below are written against the term shape
-the legacy `do` elaborator produces, destructuring with `extract_lets` the join points it
-emits as `let`s. leanprover/lean4#13305 made the new `do` elaborator the default in v4.32.0,
-and it emits `have __do_jp` join points and inlines the `if` chains instead. Pin the legacy
-elaborator here until those proofs are migrated (digama0/lean4lean#31).
--/
-set_option backward.do.legacy true
-
 namespace Lean4Lean
 open Lean
 

Lean4Lean/TypeChecker.lean

@@ -7,15 +7,6 @@ import Lean4Lean.ForEachExprV
 import Lean4Lean.EquivManager
 import Lean4Lean.FuelConfig
 
-/-
-The `Lean4Lean.Verify` proofs about the definitions below are written against the term shape
-the legacy `do` elaborator produces, destructuring with `extract_lets` the join points it
-emits as `let`s. leanprover/lean4#13305 made the new `do` elaborator the default in v4.32.0,
-and it emits `have __do_jp` join points and inlines the `if` chains instead. Pin the legacy
-elaborator here until those proofs are migrated (digama0/lean4lean#31).
--/
-set_option backward.do.legacy true
-
 namespace Lean4Lean
 open Lean hiding Environment Exception
 open Kernel

Lean4Lean/Verify/EquivManager.lean

@@ -261,21 +261,19 @@ theorem toNode.WF :
 
 theorem isEquiv.WF :
     M.WF env Us Δ m (isEquiv useHash e₁ e₂) fun b _ => b → IsDefEqE env Us Δ e₁ e₂ := by
-  unfold isEquiv; extract_lets F1 F2 F3
-  split <;> [exact .pure fun _ => ptrEqExpr_eq ‹_› ▸ .rfl; skip]
-  simp [F3]; split <;> [exact .pure nofun; skip]
-  simp [F2]; split
+  unfold isEquiv; split <;> [exact .pure fun _ => ptrEqExpr_eq ‹_› ▸ .rfl; skip]
+  split <;> [exact .pure nofun; split]
   · rename_i h; refine .pure ?_
-    unfold Expr.isBVar at h; split at h <;> cases h.1; split at h <;> cases h.2
+    simp only [Bool.and_eq_true, Expr.isBVar] at h
+    split at h <;> cases h.1; split at h <;> cases h.2
     simp [Expr.bvarIdx!]; rintro ⟨⟩; exact .rfl
-  unfold F1
   refine toNode.WF.bind fun i₁ _ _ a1 => find.WF.bind fun j₁ _ le₁ a2 => ?_
   refine toNode.WF.bind fun i₂ _ le₂ b1 => find.WF.bind fun j₂ m₀ le₃ b2 => ?_
   refine .stateWF fun wf => ?_
   replace a1 := le₁.trans le₂ |>.trans le₃ |>.toNodeMap a1
   replace a2 := le₂.trans le₃ |>.uf a2
   replace b1 := le₃.toNodeMap b1
-  extract_lets F4 F5
+  extract_lets F4
   split
   · rename_i h; simp at h; cases h; refine .pure fun _ => wf.defeq a1 b1 (a2.trans b2.symm)
   have {m b} (le₄ : m₀ ≤ m) (H : b = true → IsDefEqE env Us Δ e₁ e₂) :
@@ -288,7 +286,7 @@ theorem isEquiv.WF :
     have ⟨r₂, hr₂⟩ := wf.wf.1 <| b2.lt_size.1 <| wf.wf.2 ⟨_, b1⟩
     suffices IsDefEqE env Us Δ r₁ r₂ from have ⟨wf, h⟩ := merge.WF wf this hr₁ hr₂; ⟨wf, h, H⟩
     exact (wf.defeq a1 hr₁ a2).symm.trans <| .trans (H ‹_›) (wf.defeq b1 hr₂ b2)
-  simp; unfold F5; split
+  simp; split
   · apply this .rfl; simp; rintro rfl rfl; exact .rfl
   · apply this .rfl; simp; rintro rfl; exact .rfl
   · apply this .rfl; simp; rintro rfl; exact .rfl

Lean4Lean/Verify/TypeChecker/Basic.lean

@@ -917,7 +917,7 @@ theorem unfoldDefinitionCore.WF {c : VContext} {s : VState} (he : c.TrExprS e e'
     · exact (List.mapM_eq_some.1 a2).length_eq.symm.trans <| a3.trans b2.symm
   split <;> [rename_i h5; exact .pure this]
   refine .pureBind <| .get ?_
-  split <;> [rename_i eq; refine .pureBind ?_]
+  split <;> [rename_i eq; skip]
   · refine .stateWF fun wf => .pure ?_
     obtain ⟨_, _, _, ⟨⟩, a1, rfl⟩ := wf.unfold_wf eq
     cases h3.symm.trans a1; exact this

Lean4Lean/Verify/TypeChecker/InferType.lean

@@ -414,15 +414,15 @@ theorem inferType'.WF
     (h1 : e.FVarsIn (· ∈ c.vlctx.fvars))
     (hinf : inferOnly = true → ∃ e', c.TrExprS e e') :
     (inferType' e inferOnly).WF c s fun ty _ => ∃ e' ty', c.TrTyping e ty e' ty' := by
-  unfold inferType'; lift_lets; intro F F1 F2 --; simp
+  unfold inferType'; lift_lets; intro F F1
   split <;> [exact .throw; refine .get <| .get ?_]
   split
   · rename_i h; refine .stateWF fun wf => .pure ?_
     generalize hic : cond .. = ic at h
     have : ic.WF c s := by
       subst ic; cases inferOnly <;> [exact wf.inferTypeC_wf; exact wf.inferTypeI_wf]
     exact (this h).2.2.2.2 h1
-  generalize hP : (fun ty:Expr => _) = P
+  generalize hP : (fun _ (_ : VState) => _) = P
   have hF {ty e' ty' s} (H : c.TrTyping e ty e' ty') : (F ty).WF c s P := by
     rintro _ mwf wf a s' ⟨⟩
     refine let s' := _; ⟨s', rfl, ?_⟩
@@ -436,7 +436,7 @@ theorem inferType'.WF
     subst P; revert s'; cases inferOnly <;> (dsimp -zeta; intro s'; refine ⟨.rfl, ?_, _, _, H⟩)
     · exact { wf with inferTypeC_wf := hic wf.inferTypeC_wf }
     · exact { wf with inferTypeI_wf := hic wf.inferTypeI_wf }
-  unfold F1; refine .get ?_; split
+  split
   · extract_lets G1; split <;> [split; skip]
     · refine .getEnv <| (M.WF.liftExcept envGet.WF).lift.bind fun _ _ _ h => ?_
       have ⟨_, h, _⟩ := c.trenv.find? h <|

Lean4Lean/Verify/TypeChecker/IsDefEq.lean

@@ -15,7 +15,7 @@ theorem isDefEqLambda.WF {c : VContext} {s : VState}
       b → (c.withMLC m).IsDefEqU ei₁' ei₂' := by
   unfold isDefEqLambda; let c' := c.withMLC m
   split <;> [rename_i n₁ d₁ b₁ bi₁ n₂ d₂ b₂ bi₂; (simp [hsubst]; exact isDefEq.WF he₁ he₂)]
-  extract_lets F di₁ di₂ G; unfold G di₁ di₂
+  extract_lets F di₁ di₂; unfold di₁ di₂
   simp at he₁ he₂
   let .lam (ty' := t₁') (body' := b₁') ⟨_, a1⟩ a2 a3 := he₁
   let .lam (ty' := t₂') (body' := b₂') b1 b2 b3 := he₂
@@ -85,7 +85,7 @@ theorem isDefEqForall.WF {c : VContext} {s : VState}
       b → (c.withMLC m).IsDefEqU ei₁' ei₂' := by
   unfold isDefEqForall; let c' := c.withMLC m
   split <;> [rename_i n₁ d₁ b₁ bi₁ n₂ d₂ b₂ bi₂; (simp [hsubst]; exact isDefEq.WF he₁ he₂)]
-  extract_lets F di₁ di₂ G; unfold G di₁ di₂
+  extract_lets F di₁ di₂; unfold di₁ di₂
   simp at he₁ he₂
   let .forallE (ty' := t₁') (body' := b₁') ⟨_, a1⟩ _ a2 a3 := he₁
   let .forallE (ty' := t₂') (body' := b₂') b1 ⟨_, bT⟩ b2 b3 := he₂
@@ -164,8 +164,7 @@ theorem quickIsDefEq.WF {c : VContext} {s : VState}
     · intro h; apply (VEnv.IsDefEqU.weak'_iff c.Ewf a1 a2.toCtx).1
       exact (h1 h).uniq c.Ewf (a2.bvars_eq.trans c.mlctx.noBV)
         a1 (he₁.weakFV' c.Ewf a2 a1) (he₂.weakFV' c.Ewf a2 a1)
-  extract_lets F; split <;> [exact .pure fun _ => h ‹_›; skip]
-  refine .pureBind ?_; unfold F; split
+  split <;> [exact .pure fun _ => h ‹_›; split]
   · exact .toLBoolM <| c.withMLC_self ▸
       isDefEqLambda.WF (subst := #[]) (fvs := []) rfl (c.withMLC_self ▸ he₁) (c.withMLC_self ▸ he₂)
   · exact .toLBoolM <| c.withMLC_self ▸
@@ -238,14 +237,13 @@ theorem tryEtaStruct.WF {c : VContext} {s : VState}
 theorem isDefEqApp.WF {c : VContext} {s : VState}
     (he₁ : c.TrExprS e₁ e₁') (he₂ : c.TrExprS e₂ e₂') :
     RecM.WF c s (isDefEqApp e₁ e₂) fun b _ => b → c.IsDefEqU e₁' e₂' := by
-  unfold isDefEqApp; extract_lets F1
-  split <;> [(refine .pureBind ?_; unfold F1); exact .pure nofun]
+  unfold isDefEqApp; split <;> [skip; exact .pure nofun]
   rw [Expr.withApp_eq, Expr.withApp_eq]
   split <;> [rename_i eq; exact .pure nofun]
   have ⟨_, he₁'⟩ := AppStack.build <| e₁.mkAppList_getAppArgsList ▸ he₁
   have ⟨_, he₂'⟩ := AppStack.build <| e₂.mkAppList_getAppArgsList ▸ he₂
-  refine (isDefEq.WF he₁'.tr he₂'.tr).bind fun _ _ _ h => ?_; extract_lets F2
-  split <;> [(refine .pureBind ?_; unfold F2); exact .pure nofun]
+  refine (isDefEq.WF he₁'.tr he₂'.tr).bind fun _ _ _ h => ?_
+  split <;> [skip; exact .pure nofun]
   let rec loop.WF {s args₁ args₂ f₁ f₂ f₁' f₂' eq i} (l₁ r₁ l₂ r₂)
       (h₁ : args₁.toList = l₁ ++ r₁) (hi₁ : l₁.length = i)
       (h₂ : args₂.toList = l₂ ++ r₂) (hi₂ : l₂.length = i)
@@ -300,9 +298,9 @@ theorem isDefEqProofIrrel.WF {c : VContext} {s : VState}
     (he₁ : c.TrExprS e₁ e₁') (he₂ : c.TrExprS e₂ e₂') :
     RecM.WF c s (isDefEqProofIrrel e₁ e₂) fun b _ => b = .true → c.IsDefEqU e₁' e₂' := by
   unfold isDefEqProofIrrel
-  refine (inferType.WF he₁).bind fun _ _ _ ⟨_, a1, a2, a3, a4⟩ => ?_; extract_lets F1
+  refine (inferType.WF he₁).bind fun _ _ _ ⟨_, a1, a2, a3, a4⟩ => ?_
   refine (isProp.WF a3).bind fun _ _ _ h1 => ?_
-  split <;> [exact .pure nofun; (refine .pureBind ?_; unfold F1)]
+  split <;> [exact .pure nofun; skip]
   rename_i h; simp at h
   refine (inferType.WF he₂).bind fun _ _ _ ⟨_, b1, b2, b3, b4⟩ => .toLBoolM ?_
   refine (isDefEq.WF a3 b3).mono fun _ _ _ h2 hb => ?_
@@ -316,9 +314,8 @@ theorem cacheFailure.WF {c : VContext} {s : VState} :
 theorem tryUnfoldProjApp.WF {c : VContext} {s : VState} (he : c.TrExprS e e') :
     (tryUnfoldProjApp e).WF c s fun oe _ =>
     ∀ e₁, oe = some e₁ → c.FVarsBelow e e₁ ∧ c.TrExpr e₁ e' := by
-  unfold tryUnfoldProjApp; extract_lets f F
+  unfold tryUnfoldProjApp; extract_lets f
   split <;> [exact .pure nofun; skip]
-  refine .pureBind ?_; unfold F
   refine (whnfCore.WF he).bind fun _ _ _ h => ?_
   refine .pure fun _ => ?_
   split <;> rintro ⟨⟩; exact h
@@ -420,11 +417,11 @@ theorem isNatSuccOf?_wf {c : VContext} (H : isNatSuccOf? e = some e₁)
 theorem isDefEqOffset.WF {c : VContext} {s : VState}
     (he₁ : c.TrExprS e₁ e₁') (he₂ : c.TrExprS e₂ e₂') :
     (isDefEqOffset e₁ e₂).WF c s fun b _ => b = .true → c.IsDefEqU e₁' e₂' := by
-  unfold isDefEqOffset; extract_lets F; split
+  unfold isDefEqOffset; split
   · rename_i h; simp at h
     cases isNatZero_wf h.1 he₁; cases isNatZero_wf h.2 he₂
     exact .pure fun _ => .refl <| he₁.wf c.Ewf c.Δwf
-  · refine .pureBind ?_; unfold F; split <;> [skip; exact .pure nofun]
+  · split <;> [skip; exact .pure nofun]
     obtain ⟨_, a1, rfl⟩ := isNatSuccOf?_wf ‹_› he₁
     obtain ⟨_, b1, rfl⟩ := isNatSuccOf?_wf ‹_› he₂
     refine .toLBoolM <| (isDefEqCore.WF a1 b1).mono fun _ _ _ h hb => ?_
@@ -436,11 +433,11 @@ theorem lazyDeltaReduction.loop.WF {c : VContext} {s : VState}
     (he₁ : c.TrExprS e₁ e₁') (he₂ : c.TrExprS e₂ e₂') :
     (lazyDeltaReduction.loop e₁ e₂ n).WF c s fun r _ => r.WF c e₁' e₂' := by
   induction n generalizing s e₁ e₂ e₁' e₂' with | zero => exact .throw | succ n ih
-  unfold loop; extract_lets F1 F2 F3
+  unfold loop; extract_lets F1
   refine (isDefEqOffset.WF he₁ he₂).bind fun _ _ _ h => ?_; split
   · exact .pure fun hb => h (by simpa using hb)
-  suffices hF2 : ∀ {s}, (F2 ⟨⟩).WF c s fun r _ => r.WF c e₁' e₂' by
-    refine .pureBind <|.readThe ?_; split <;> [skip; exact hF2]
+  suffices hF1 : ∀ {s}, (F1 ⟨⟩).WF c s fun r _ => r.WF c e₁' e₂' by
+    refine .readThe ?_; split <;> [skip; exact hF1]
     refine (reduceNat.WF he₁).bind fun _ _ _ h => ?_; split
     · have ⟨_, a1, a2⟩ := (h _ rfl).2
       refine (isDefEqCore.WF a1 he₂).bind fun _ _ _ h => .pure fun hb => ?_
@@ -449,13 +446,12 @@ theorem lazyDeltaReduction.loop.WF {c : VContext} {s : VState}
     · have ⟨_, a1, a2⟩ := (h _ rfl).2
       refine (isDefEqCore.WF he₁ a1).bind fun _ _ _ h => .pure fun hb => ?_
       exact (h hb).trans c.Ewf c.Δwf a2
-    exact hF2
-  intro s; unfold F2; refine .getEnv ?_
+    exact hF1
+  intro s; unfold F1; refine .getEnv ?_
   refine (M.WF.liftExcept reduceNative.WF).lift.bind fun _ _ _ h => ?_
   split <;> [cases h _ rfl; skip]
   refine (M.WF.liftExcept reduceNative.WF).lift.bind fun _ _ _ h => ?_
   split <;> [cases h _ rfl; skip]
-  refine .pureBind ?_; unfold F1
   refine (lazyDeltaReductionStep.WF he₁ he₂).bind fun r _ _ h => ?_
   obtain r|r|r := r
   · let ⟨_, ⟨_, a1, a2⟩, ⟨_, b1, b2⟩⟩ := h
@@ -484,11 +480,11 @@ theorem isDefEqUnitLike.WF {c : VContext} {s : VState}
 theorem isDefEqCore'.WF {c : VContext} {s : VState}
     (he₁ : c.TrExprS e₁ e₁') (he₂ : c.TrExprS e₂ e₂') :
     RecM.WF c s (isDefEqCore' e₁ e₂) fun b _ => b = true → c.IsDefEqU e₁' e₂' := by
-  unfold isDefEqCore'; extract_lets F1 F2 F3
+  unfold isDefEqCore'; extract_lets F1
   refine (quickIsDefEq.WF he₁ he₂).bind fun _ _ _ h => ?_
   split <;> [exact .pure fun hb => h (by simpa using hb); skip]
-  refine .pureBind <| .readThe ?_
-  suffices ∀ {s}, RecM.WF c s (F2 ⟨⟩) fun b _ => b = true → c.IsDefEqU e₁' e₂' by
+  refine .readThe ?_
+  suffices ∀ {s}, RecM.WF c s (F1 ⟨⟩) fun b _ => b = true → c.IsDefEqU e₁' e₂' by
     split <;> [rename_i h1; exact this]
     refine (whnf.WF he₁).bind fun _ _ _ ⟨_, _, a1, a2⟩ => ?_
     split <;> [rename_i h2; exact this]
@@ -501,29 +497,29 @@ theorem isDefEqCore'.WF {c : VContext} {s : VState}
     cases c.hasPrimitives.boolTrue c1
     simp at b3 c3; subst b3 c3; simp at b2 c2; subst b2 c2
     exact a2.symm
-  intro; unfold F2
+  intro; unfold F1
   refine (whnfCore.WF he₁).bind fun _ _ _ ⟨_, e₁', a1, a2⟩ => ?_
   refine (whnfCore.WF he₂).bind fun _ _ _ ⟨_, e₂', b1, b2⟩ => ?_
-  extract_lets F2 F3
+  extract_lets F2
   refine .mono (Q := fun b _ => b = true → c.IsDefEqU e₁' e₂') ?_ fun _ _ _ h hb =>
     a2.symm.trans c.Ewf c.Δwf (h (by simpa using hb)) |>.trans c.Ewf c.Δwf b2
-  suffices ∀ {s}, RecM.WF c s (F3 ⟨⟩) fun b _ => b = true → c.IsDefEqU e₁' e₂' by
+  suffices ∀ {s}, RecM.WF c s (F2 ⟨⟩) fun b _ => b = true → c.IsDefEqU e₁' e₂' by
     split <;> [skip; exact this]
     refine (quickIsDefEq.WF a1 b1).bind fun _ _ _ h => ?_
     split <;> [skip; exact this]
     exact .pure fun hb => h (by simpa using hb)
-  intro; unfold F3
+  intro; unfold F2
   refine (isDefEqProofIrrel.WF a1 b1).bind fun _ _ _ h => ?_
   split
   · exact .pure fun hb => h (by simpa using hb)
-  refine .pureBind <| (lazyDeltaReduction.loop.WF a1 b1).readThe.bind fun _ _ _ h => ?_; split
+  refine (lazyDeltaReduction.loop.WF a1 b1).readThe.bind fun _ _ _ h => ?_; split
   · cases h.1
   · exact .pure h
   have ⟨⟨e₁', c1, c4⟩, ⟨e₂', d1, d4⟩⟩ := h
   refine .mono (Q := fun b _ => b = true → c.IsDefEqU e₁' e₂') ?_ fun _ _ _ h hb =>
     c4.symm.trans c.Ewf c.Δwf (h (by simpa using hb)) |>.trans c.Ewf c.Δwf d4
-  extract_lets F2 F3 F4 F5 F6 F7
-  suffices ∀ {s}, RecM.WF c s (F7 ⟨⟩) fun b _ => b = true → c.IsDefEqU e₁' e₂' by
+  extract_lets F3
+  suffices ∀ {s}, RecM.WF c s (F3 ⟨⟩) fun b _ => b = true → c.IsDefEqU e₁' e₂' by
     split
     · split <;> [rename_i h2; exact this]
       refine .pure fun _ => ?_
@@ -545,20 +541,20 @@ theorem isDefEqCore'.WF {c : VContext} {s : VState}
       simp at h2; subst h2; clear h
       exact .pure fun _ => c2.uniq c.Ewf (.refl c.Δwf) d2 (h ‹_›)
     · exact this
-  intro; unfold F7
+  intro; unfold F3
   refine (whnfCore.WF c1).bind fun _ _ _ ⟨_, e₁'', c5, c6⟩ => ?_
   refine (whnfCore.WF d1).bind fun _ _ _ ⟨_, e₂'', d5, d6⟩ => ?_
   split
-  · exact (isDefEqCore.WF c5 d5).bind fun _ _ _ h => .pure fun hb =>
+  · exact (isDefEqCore.WF c5 d5).mono fun _ _ _ h hb =>
       c6.symm.trans c.Ewf c.Δwf (h (by simpa using hb)) |>.trans c.Ewf c.Δwf d6
-  refine .pureBind <| (isDefEqApp.WF c1 d1).bind fun _ _ _ h => ?_
+  refine (isDefEqApp.WF c1 d1).bind fun _ _ _ h => ?_
   split <;> [exact .pure fun _ => h ‹_›; skip]
-  refine .pureBind <| (tryEtaExpansion.WF c1 d1).bind fun _ _ _ h => ?_
+  refine (tryEtaExpansion.WF c1 d1).bind fun _ _ _ h => ?_
   split <;> [exact .pure fun _ => h ‹_›; skip]
-  refine .pureBind <| (tryEtaStruct.WF c1 d1).bind fun _ _ _ h => ?_
+  refine (tryEtaStruct.WF c1 d1).bind fun _ _ _ h => ?_
   split <;> [exact .pure fun _ => h ‹_›; skip]
-  refine .pureBind <| (tryStringLitExpansion.WF c1 d1).bind fun _ _ _ h => ?_
+  refine (tryStringLitExpansion.WF c1 d1).bind fun _ _ _ h => ?_
   split <;> [exact .pure fun hb => h (by simpa using hb); skip]
-  refine .pureBind <| (isDefEqUnitLike.WF c1 d1).bind fun _ _ _ h => ?_
+  refine (isDefEqUnitLike.WF c1 d1).bind fun _ _ _ h => ?_
   split <;> [exact .pure fun _ => h ‹_›; skip]
-  exact .pureBind <| .pure nofun
+  exact .pure nofun

Lean4Lean/Verify/TypeChecker/Reduce.lean

@@ -1,13 +1,5 @@
 import Lean4Lean.Verify.TypeChecker.Basic
 
-/-
-This file states `RecM.WF` goals with `do` blocks that have to match the shape the
-definitions in `Lean4Lean.TypeChecker` elaborate to, which is pinned to the legacy `do`
-elaborator (leanprover/lean4#13305). Pin it here too so the two agree
-(digama0/lean4lean#31).
--/
-set_option backward.do.legacy true
-
 namespace Lean4Lean.TypeChecker.Inner
 open Lean hiding Environment Exception
 open Kernel
@@ -102,23 +94,9 @@ theorem reduceNat.WF {c : VContext} (he : c.TrExprS e e') :
   replace hprims {a} : Environment.primitives.contains a ↔ a ∈ prims := by
     simp [hprims, NameSet.contains, NameSet.ofList]
   unfold reduceNat; extract_lets nargs F1 fn
-  split <;> (split <;> [skip; exact hP ▸ .pure nofun])
-  · rename_i h1 h2
-    simp [nargs, Expr.getAppNumArgs_eq] at h1; subst fn
-    let .app f a := e; simp [Expr.appFn!, Expr.eqv_const] at h2 ⊢; subst h2
-    let .app ha1 ha2 hf ha := he
-    let .const h1 h2 h3 := hf
-    refine (whnf.WF ha).bind fun a₁ _ _ ⟨a1, _, a2, a3⟩ => ?_
-    split <;> [rename_i n h; exact hP ▸ .pure nofun]
-    obtain ⟨hn, rfl⟩ := rawNatLitExt?.WF h a2
-    refine hP ▸ .pure ?_; rintro _ ⟨⟩; refine ⟨fun _ _ _ => trivial, ?_⟩
-    have ⟨ci, c1, _⟩ := c.trenv.find?_iff.2 ⟨_, h1⟩
-    have ⟨c2, c3⟩ := c.safePrimitives c1 <| hprims.2 (by simp [prims])
-    have ⟨d1, d2, d3⟩ := c.trenv.find?_uniq c1 h1; cases h2
-    refine have ⟨p1, p2⟩ := TrExprS.natLit c.hasPrimitives hn _; ⟨_, p1, ?_⟩
-    refine p2.toU.symm.trans c.Ewf c.Δwf ?_
-    exact ⟨_, ha1.appDF <| a3.of_r c.Ewf c.Δwf ha2⟩
-  · split <;> [rename_i f ls a b _ h2; exact hP ▸ .pure nofun]
+  cases h1 : nargs == 1 <;> simp only [Bool.false_eq_true, ↓reduceIte]
+  · cases nargs == 2 <;> [exact hP ▸ .pure nofun; simp only [↓reduceIte]]
+    split <;> [rename_i f ls a b; exact hP ▸ .pure nofun]
     have hfun guard {g fc G} [DecidableRel guard] (hprim : fc ∈ prims)
         (heval : c.venv.ReflectsNatNatNat fc g) (hG : RecM.WF c s G P) :
         RecM.WF c s (do if f == fc then {return ← reduceBinNatOpG guard g a b}; G) P := by
@@ -146,3 +124,18 @@ theorem reduceNat.WF {c : VContext} (he : c.TrExprS e e') :
     apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natShiftLeft
     apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natShiftRight
     exact hP ▸ .pure nofun
+  · split <;> [rename_i h2; exact hP ▸ .pure nofun]
+    simp [nargs, Expr.getAppNumArgs_eq] at h1; subst fn
+    let .app f a := e; simp [Expr.appFn!, Expr.eqv_const] at h2 ⊢; subst h2
+    let .app ha1 ha2 hf ha := he
+    let .const h1 h2 h3 := hf
+    refine (whnf.WF ha).bind fun a₁ _ _ ⟨a1, _, a2, a3⟩ => ?_
+    split <;> [rename_i n h; exact hP ▸ .pure nofun]
+    obtain ⟨hn, rfl⟩ := rawNatLitExt?.WF h a2
+    refine hP ▸ .pure ?_; rintro _ ⟨⟩; refine ⟨fun _ _ _ => trivial, ?_⟩
+    have ⟨ci, c1, _⟩ := c.trenv.find?_iff.2 ⟨_, h1⟩
+    have ⟨c2, c3⟩ := c.safePrimitives c1 <| hprims.2 (by simp [prims])
+    have ⟨d1, d2, d3⟩ := c.trenv.find?_uniq c1 h1; cases h2
+    refine have ⟨p1, p2⟩ := TrExprS.natLit c.hasPrimitives hn _; ⟨_, p1, ?_⟩
+    refine p2.toU.symm.trans c.Ewf c.Δwf ?_
+    exact ⟨_, ha1.appDF <| a3.of_r c.Ewf c.Δwf ha2⟩