feat: port the mvcgen' tactic to the new Std.Internal.Do meta theory (#14015)

This PR ports the experimental `mvcgen'` tactic to the new
`Std.Internal.Do` meta theory, where verification-condition generation
works on lattice entailments `pre ⊑ wp x post epost`. Two changes are
visible at the proof surface: `mvcgen'` now eagerly introduces all state
components as local hypotheses, so more facts reach `grind`; and loop
invariants no longer have to restate the exceptional postcondition.

Previously the invariant for a loop that can throw had to repeat the
exception condition alongside the actual invariant:
```lean
theorem throwing_loop_spec :
    ⦃fun s => ⌜s = 4⌝⦄
    throwing_loop
    ⦃post⟨fun _ _ => ⌜False⌝,
          fun e s => ⌜e = 42 ∧ s = 4⌝⟩⦄ := by
  mvcgen' [throwing_loop]
  case inv1 => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝,
                         fun e s => ⌜e = 42 ∧ s = 4⌝⟩
```
Now the exceptional postcondition is taken from the surrounding
`Triple`, so the invariant case carries only the invariant:
```lean
theorem throwing_loop_spec :
    ⦃fun s => s = 4⦄
    throwing_loop
    ⦃fun _ _ => False;
     fun e s => e = 42 ∧ s = 4⦄ := by
  mvcgen' [throwing_loop]
  case inv1 => exact ⟨fun (xs, r) s => r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⟩
```

The spec lemmas in `Std.Internal.Do.Triple.SpecLemmas` are registered
with `@[spec]` and populate the new spec database, which also gains the
`whileM`/`Lean.Loop` specifications, `Invariant.withEarlyReturnNewDo`,
and pointwise entailment lemmas for state introduction.

The port replays Vladimir Gladshtein's #13978 onto master's file
structure.

The solver diverges from the legacy algorithm in three points.
Reflexivity runs on every entailment before the pure-precondition lifts,
closing the leaf VCs where a spec precondition meets an identical goal
precondition (`Q x ⊑ wp (pure x) Q E` ends in `Q x ⊑ Q x`) and
instantiating spec parameters that occur only in rule premises.
Reflexivity no longer assigns synthetic opaque metavariables, so
function-typed invariant holes are not silently solved away. Pure
preconditions are lifted into the local context as soon as they arise;
the lifted hypothesis is cached in `Scope.lastLiftedPre?`, and a
targeted assumption step closes the handoff VCs of subsequent spec
applications against it.

This is the second of two steps that land `vova/new-mvcgen` onto master.
The first step (#13954) updated the `@[spec]` builtin attribute and
regenerated `stage0`, so this PR reuses master's `stage0` and contains
no generated C changes. Invariant suggestion (`invariants?`) yields no
suggestions on the new surface; porting the suggestion analysis is
deferred until `mvcgen'` replaces the legacy `mvcgen`.

---------

Co-authored-by: volodeyka <vovaglad00@gmail.com>

Author: sgraf812

src/Lean/Elab/Tactic/Do/Internal/VCGen.lean

@@ -10,6 +10,7 @@ public import Lean.Elab.Tactic.Do.Internal.VCGen.Reduce
 public import Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB
 public import Lean.Elab.Tactic.Do.Internal.VCGen.RuleConstruction
 public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
+public import Lean.Elab.Tactic.Do.Internal.VCGen.EPost
 public import Lean.Elab.Tactic.Do.Internal.VCGen.Util
 public import Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache
 public import Lean.Elab.Tactic.Do.Internal.VCGen.Entails
@@ -21,12 +22,13 @@ public import Lean.Elab.Tactic.Do.Internal.VCGen.Frontend
 The `mvcgen'` tactic, split across the modules above.
 
 - `VCGen.Reduce` — SymM head-redex reducer.
-- `VCGen.SpecDB` — `SpecTheoremNew`/`SpecTheoremsNew` + database operations.
+- `VCGen.SpecDB` — `SpecTheorem` instantiation, simp-side migration, and `findSpecs` lookup.
 - `VCGen.RuleConstruction` — SymM rule constructors from spec/simp/split info.
 - `VCGen.Context` — `VCGenM`, its `Context`/`State`, the bundle of pre-built rules.
-- `VCGen.Util` — generic VCGenM helpers (`introsSimp`, `repeatAndRfl`, app builders).
+- `VCGen.EPost` — exception-postcondition decomposition helpers.
+- `VCGen.Util` — generic VCGenM helpers (`introsHygienic`, `simpGoalTelescope`, `solveTrivialConjuncts`).
 - `VCGen.RuleCache` — VCGenM cache wrappers around the SymM rule constructors.
-- `VCGen.Entails` — entailment-shaped goal decomposition (`solveSPredEntails` etc.).
+- `VCGen.Entails` — entailment-shaped goal decomposition (Triple unfolding, state/precondition intro, EPost and lattice steps).
 - `VCGen.Solve` — the main `solve` step / `SolveResult`.
 - `VCGen.Driver` — the worklist driver (`work`, `emitVC`, `main`, `Result`).
 - `VCGen.Frontend` — the `mvcgen'` syntax + tactic elaborator + `mkSpecContext`.

src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
+Authors: Sebastian Graf, Vladimir Gladshtein
 -/
 module
 
@@ -14,8 +14,7 @@ public import Lean.Meta.Sym.Simp.SimpM
 public import Lean.Meta.Tactic.Grind.Types
 
 open Lean Meta Elab Tactic Sym
-open Lean.Elab.Tactic.Do Lean.Elab.Tactic.Do.SpecAttr
-open Std.Do
+open Lean.Elab.Tactic.Do Lean.Elab.Tactic.Do.Internal.SpecAttr
 
 namespace Lean.Elab.Tactic.Do.Internal
 
@@ -45,48 +44,69 @@ public def UntilPatternThunk.force (ref : IO.Ref UntilPatternThunk) (m : Expr) :
     ref.set (.elaborated pat)
     return pat
 
+/--
+Common metadata for a goal whose right-hand side is a weakest-precondition application
+`pre ⊑ wp m Pred EPred monadInst instAL instEAL instWP α prog post epost s₁ ... sₙ`.
+-/
+public structure VCGen.WPInfo where
+  /-- The `wp` function head, separated from its explicit core arguments. -/
+  head : Expr
+  /-- The ordered core arguments of the `wp` application:
+  `#[m, Pred, EPred, monadInst, instAL, instEAL, instWP, α, prog, post, epost]`. -/
+  args : Array Expr
+  /-- Extra arguments applied after `wp … prog post epost`, usually concrete state arguments. -/
+  excessArgs : Array Expr
+
+namespace VCGen.WPInfo
+
+/-- Monad type constructor argument of `wp`. -/
+public def m (info : WPInfo) : Expr := info.args[0]!
+/-- Predicate/lattice type argument of `wp`. -/
+public def Pred (info : WPInfo) : Expr := info.args[1]!
+/-- Exception postcondition type argument of `wp`. -/
+public def EPred (info : WPInfo) : Expr := info.args[2]!
+/-- `WPMonad` instance argument of `wp`. -/
+public def instWP (info : WPInfo) : Expr := info.args[6]!
+/-- Program expression classified by VCGen. -/
+public def prog (info : WPInfo) : Expr := info.args[8]!
+
+end VCGen.WPInfo
+
+/-- Pre-built backward rules for the introduction steps of `solve`. -/
+public structure VCGen.IntroRules where
+  /-- The backward rule for `Triple.intro`. Unfolds `⦃P⦄ x ⦃Q; E⦄` into `P ⊑ wp x Q E`. -/
+  tripleIntro : BackwardRule
+  /-- The backward rule for `Lean.Order.le_of_forall_le`. Peels one excess state argument
+  from a function-lattice entailment. -/
+  stateArgIntro : BackwardRule
+  /-- The backward rule for `Lean.Order.le_of_imp_top_le`. Introduces a bare pure
+  precondition on the `Prop` lattice. -/
+  propPreIntro : BackwardRule
+  /-- The backward rule for `Lean.Order.ofProp_le`. Introduces an embedded pure
+  precondition `⌜p⌝` on any complete lattice. -/
+  ofPropPreIntro : BackwardRule
+  /-- The backward rule for `Lean.Order.true_le_of_top_le`. Replaces a `True` precondition
+  with `⊤` on the `Prop` lattice. -/
+  truePreIntro : BackwardRule
+
 public structure VCGen.Context where
-  /-- The backward rule for `SPred.entails_cons_intro`. -/
-  entailsConsIntroRule : BackwardRule
-  /-- The backward rule for `SPred.entails_nil_pure_intro`. Preferred over `entails_nil_intro`
-  when the LHS is `⌜φ⌝`, as it unwraps `.down` on the pure assertion. -/
-  entailsNilPureIntroRule : BackwardRule
-  /-- The backward rule for `SPred.entails_nil_intro`. Fallback when LHS is not `⌜φ⌝`. -/
-  entailsNilIntroRule : BackwardRule
-  /-- The backward rule for `SPred.apply_pure_cons_entails_l`. Peels a state arg from
-  `SPred.pure (σ::σs) φ s` on the LHS of an entailment. -/
-  applyPureConsEntailsLRule : BackwardRule
-  /-- The backward rule for `SPred.apply_pure_cons_entails_r`. Peels a state arg from
-  `SPred.pure (σ::σs) φ s` on the RHS of an entailment. -/
-  applyPureConsEntailsRRule : BackwardRule
-  /-- The backward rule for `SPred.down_pure_intro`. Reduces a target of the form
-  `(SPred.pure [] φ).down` to `φ`. -/
-  downPureIntroRule : BackwardRule
-  /-- The backward rule for `SPred.pure_elim'`. -/
-  pureElimRule : BackwardRule
-  /-- The backward rule for `SPred.pure_intro`. -/
-  pureIntroRule : BackwardRule
-  /-- The backward rule for `PostCond.entails.rfl`. Tried first to close by reflexivity. -/
-  postCondEntailsRflRule : BackwardRule
-  /-- The backward rule for `PostCond.entails.mk`. -/
-  postCondEntailsMkRule : BackwardRule
-  /-- The backward rule for `ExceptConds.entails.rfl`. -/
-  exceptCondsEntailsRflRule : BackwardRule
-  /-- The backward rule for `ExceptConds.entails.pure`. Closes the exception side for
-  pure PostShapes, where `ExceptConds.entails` reduces to `True`. -/
-  exceptCondsEntailsPureRule : BackwardRule
-  /-- The backward rule for `ExceptConds.entails_false`. -/
-  exceptCondsEntailsFalseRule : BackwardRule
-  /-- The backward rule for `ExceptConds.entails_true`. -/
-  exceptCondsEntailsTrueRule : BackwardRule
-  /-- The backward rule for `Triple.of_entails_wp`. -/
-  tripleOfEntailsWPRule : BackwardRule
+  /-- Pre-built backward rules for the introduction steps of `solve`. -/
+  introRules : VCGen.IntroRules
+  /-- The backward rule for `Lean.Order.top_le_prop`. Strips a `(⊤ : Prop) ⊑ ·` wrapper
+  from a VC before it is emitted. -/
+  elimPreRule : BackwardRule
   /-- The backward rule for `And.intro`. -/
   andIntroRule : BackwardRule
+  /-- The backward rule for `Lean.Order.PartialOrder.rel_refl`. Closes a reflexive
+  entailment `pre ⊑ pre`. -/
+  reflRule : BackwardRule
+  /-- The backward rule for `meet_top_le_of_le`. Cancels a redundant `⊓ ⊤` on the left of an
+  entailment, turning `P ⊓ ⊤ ⊑ Q` into `P ⊑ Q`. -/
+  meetTopRule : BackwardRule
   /-- User-customizable simp methods used to pre-simplify hypotheses. -/
   hypSimpMethods : Option Sym.Simp.Methods := none
   /-- The `trivial` config option: when `true` (default), `Driver.emitVC` runs
-  `repeatAndRfl` to collapse trivial `And.intro` chains; when `false`, the goal is
+  `solveTrivialConjuncts` to collapse trivial `And.intro` chains; when `false`, the goal is
   emitted as-is. -/
   trivial : Bool := true
   /-- The `jp` config option: when `true`, `tryLetIntro` recognises `__do_jp` lets
@@ -119,18 +139,21 @@ public structure VCGen.Context where
 
 public structure VCGen.Scope where
   /-- Spec database in scope: globals plus locals from in-scope hypotheses. -/
-  specs : SpecTheoremsNew
+  specs : SpecTheorems
   /-- `__do_jp` fvars currently in scope. -/
   jps : FVarIdMap JumpSiteInfo := {}
+  /-- The most recently lifted pure precondition. `tryLiftedHyp` closes handoff VCs against
+  it without walking the local context. -/
+  lastLiftedPre? : Option FVarId := none
   /-- Index of the next local declaration to consider for local specs. -/
   nextDeclIdx : Nat := 0
   deriving Inhabited
 
 public structure VCGen.State where
   /--
   A cache mapping registered SpecThms to their backward rule to apply.
-  The particular rule depends on the theorem name, the monad and the number of excess state
-  arguments that the weakest precondition target is applied to.
+  The particular rule depends on the theorem name, the `WPMonad` instance and the number of
+  excess state arguments that the weakest precondition target is applied to.
   -/
   specBackwardRuleCache : Std.HashMap (Name × Expr × Nat) BackwardRule := {}
   /--
@@ -140,6 +163,12 @@ public structure VCGen.State where
   -/
   splitBackwardRuleCache : Std.HashMap (Name × Expr × Nat) BackwardRule := {}
   /--
+  A cache mapping lattice connectives to their backward rule to apply.
+  The particular rule depends on the rule name, the monad, and the number of excess state
+  arguments that the weakest precondition target is applied to.
+  -/
+  latticeBackwardRuleCache : Std.HashMap (Name × Array Expr × Nat) BackwardRule := {}
+  /--
   Holes of type `Invariant` that have been generated so far.
   -/
   invariants : Array MVarId := #[]
@@ -178,8 +207,8 @@ public def Scope.registerJP (s : Scope) (fv : FVarId) (info : JumpSiteInfo) : Sc
 public def Scope.knownJP? (s : Scope) (fv : FVarId) : Option JumpSiteInfo :=
   s.jps.get? fv
 
-public def Scope.insertSpec (s : Scope) (thm : SpecTheoremNew) : Scope :=
-  { s with specs := { s.specs with specs := Sym.insertPattern s.specs.specs thm.pattern thm } }
+public def Scope.insertSpec (s : Scope) (thm : SpecTheorem) : Scope :=
+  { s with specs := s.specs.insert thm }
 
 /-- Walk `goal`'s local context from `scope.nextDeclIdx` onward, registering any
 spec-shaped hypotheses as local specs. Advances `nextDeclIdx` to the current
@@ -191,7 +220,7 @@ public def Scope.collectLocalSpecs (scope : Scope) (goal : MVarId) : VCGenM Scop
     let scope ← lctx.foldlM (init := scope) (start := scope.nextDeclIdx) fun scope decl => do
       if decl.isAuxDecl then return scope
       try
-        if let some thm ← mkSpecTheoremNew (.local decl.fvarId) (eval_prio low) then
+        if let some thm ← mkSpecTheoremFromLocal decl.fvarId (eval_prio low) then
           return scope.insertSpec thm
       catch _ => pure ()
       return scope

src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean

@@ -13,7 +13,6 @@ public import Lean.Meta.Sym.Grind
 
 open Lean Meta Elab Tactic Sym
 open Lean.Elab.Tactic.Do.SpecAttr
-open Std.Do
 
 namespace Lean.Elab.Tactic.Do.Internal
 
@@ -82,15 +81,18 @@ private def handleInvariantSubgoals (subgoals : List MVarId) : VCGenM (Array MVa
 Called when decomposing the goal further did not succeed; in this case we emit a VC for the goal.
 Invariant subgoals are handled separately by `handleInvariantSubgoals` directly inside `work`,
 so they never reach this path.
+If the goal is `(⊤ : Prop) ⊑ φ`, the `⊤ ⊑` wrapper is stripped first.
 -/
 public def emitVC (goal : Grind.Goal) : VCGenM Unit := do
-  let goal ← processHypotheses goal
+  let mvarId ← elimTopPre goal.mvarId
+  let mut goal := { goal with mvarId }
+  goal ← processHypotheses goal
   if goal.inconsistent then return
-  -- `trivial`: when false, skip `repeatAndRfl` (which collapses And-chains via rfl);
+  -- `trivial`: when false, skip `solveTrivialConjuncts` (which collapses And-chains via rfl);
   -- emit the goal as-is.
   let mvarId ←
     if (← read).trivial then
-      let some mvarId ← repeatAndRfl goal.mvarId | return
+      let some mvarId ← solveTrivialConjuncts goal.mvarId | return
       pure mvarId
     else
       pure goal.mvarId
@@ -109,20 +111,16 @@ public def work (scope : Scope) (goal : Grind.Goal) : VCGenM Unit := do
     let goal := s.goal
     if goal.inconsistent then continue
     match ← solve s.scope goal.mvarId with
-    | .stop =>
+    | .stop _reason =>
       emitVC goal
-    | .noEntailment .. | .noProgramFoundInTarget .. =>
-      emitVC goal
-    | .noSpecFoundForProgram prog monad thms =>
-      if (← read).errorOnMissingSpec then goal.mvarId.withContext do
+    | .noSpecFoundForProgram prog monad thms => goal.mvarId.withContext do
+      if (← read).errorOnMissingSpec then
         if thms.isEmpty then
           throwError "No spec found for program {prog}."
         else
           throwError "No spec matching the monad {monad} found for program {prog}. Candidates were {thms.map (·.proof)}."
       else
         emitVC goal
-    | .noStrategyForProgram prog => goal.mvarId.withContext do
-      throwError "Did not know how to decompose weakest precondition for {prog}"
     | .goals scope subgoals =>
       -- Handle invariant subgoals eagerly here, so that VC subgoals popped
       -- from the worklist later see the invariant MVar already assigned.
@@ -150,7 +148,7 @@ public structure Result where
   inlineHandledInvariants : Std.HashSet Nat := {}
 
 /--
-Generate verification conditions for a goal of the form `P ⊢ₛ wp⟦e⟧ Q s₁ ... sₙ` by repeatedly
+Generate verification conditions for a goal of the form `pre ⊑ wp e post epost s₁ ... sₙ` by repeatedly
 decomposing `e` using registered `@[spec]` theorems.
 Return the VCs and invariant goals.
 

src/Lean/Elab/Tactic/Do/Internal/VCGen/EPost.lean

@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vladimir Gladshtein, Sebastian Graf
+-/
+module
+
+prelude
+public import Lean.Meta.Sym
+public import Std.Internal.Do
+public import Lean.Meta.Tactic.Replace
+
+open Lean Meta Sym
+open Std.Internal.Do Lean.Order
+
+namespace Lean.Elab.Tactic.Do.Internal
+
+namespace VCGen
+
+/-!
+Helpers for decomposing exception-postcondition (`EPost`) goals: reducing an `EPost.Cons.head`
+projection in the RHS of an entailment to the underlying component. The concrete case
+(`epost⟨…⟩`) is handled by `mkEPostAtIndex`/`peelEPostTailChain`; the `⊥` case is handled by
+`replaceEPostHeadBot?`, which rewrites `pre ⊑ ⊥.head x₁ … xₙ` to `pre ⊑ ⊥`.
+-/
+
+/-- Get the `index`-th component from an `EPost` target. -/
+public def mkEPostAtIndex (target : Expr) (index : Nat) : SymM (Option Expr) := do
+  let mut curr := target
+  for _ in [:index] do
+    let_expr EPost.Cons.mk _ _ _ tail := curr | return none
+    curr := tail
+  let_expr EPost.Cons.mk _ _ head _ := curr | return none
+  return head
+
+/-- Peel a chain of `.tail` projections, returning the base `EPost` and the number of tails. -/
+public partial def peelEPostTailChain (curr : Expr) (idx : Nat := 0) : Expr × Nat :=
+  curr.consumeMData.withApp fun fn args =>
+    if fn.isConstOf ``EPost.Cons.tail && args.size > 0 then
+      peelEPostTailChain args[args.size - 1]! (idx + 1)
+    else
+      (curr, idx)
+
+/--
+When the exception postcondition is `⊥`, the RHS of a `pre ⊑ EPost.Cons.head ⊥ x₁ … xₙ` goal is
+propositionally—but not definitionally—equal to `⊥`. This rewrites the goal to `pre ⊑ ⊥`,
+constructing the equality proof from `EPost.Cons.head_bot` (for the head projection) and
+`bot_apply` (for each excess argument).
+
+The proof term is built directly with `mkApp`/`mkConst` and instances extracted from the existing
+goal, avoiding `mkAppM`/instance synthesis (which is both expensive and unable to unify `max`-of-
+universe-variable instance levels in the abstract-monad setting).
+
+`head`/`args` come from `rhs.withApp`, where `rhs = EPost.Cons.head eh et ⊥ x₁ … xₙ`, and `target`
+is the full `pre ⊑ rhs` entailment. Returns the rewritten goal, or `none` if `args[2]` is not `⊥`
+or the lattice instances are not in the expected shape (the caller then falls through). -/
+public def replaceEPostHeadBot? (goal : MVarId) (target head : Expr) (args : Array Expr) :
+    SymM (Option MVarId) := do
+  let some eh := args[0]? | return none
+  let some et := args[1]? | return none
+  let some epostArg := args[2]? | return none
+  -- `epostArg = @bot (EPost.Cons eh et) (scopedCCPO (instCompleteLattice eh et chInst ctInst))`
+  let_expr Lean.Order.bot _ botCCPOInst := epostArg | return none
+  unless botCCPOInst.isApp do return none
+  let clArgs := botCCPOInst.appArg!.getAppArgs
+  unless clArgs.size ≥ 2 do return none
+  let chInst := clArgs[clArgs.size - 2]!
+  let ctInst := clArgs[clArgs.size - 1]!
+  let [u, v] := head.constLevels! | return none
+  -- `p0 : EPost.Cons.head ⊥ = (⊥ : eh)`
+  let headBot := mkApp3 head eh et epostArg
+  let p0 := mkApp4 (mkConst ``EPost.Cons.head_bot [u, v]) eh et chInst ctInst
+  let some (_, _, b0) := (← Sym.inferType p0).eq? | return none
+  -- Fold `bot_apply` over the excess arguments: `acc : EPost.Cons.head ⊥ x₁ … xᵢ = ⊥`.
+  let mut acc := p0
+  let mut curHead := headBot
+  let mut curBot := b0
+  let mut curTy := eh
+  let mut curCL := chInst
+  for x in args.extract 3 args.size do
+    let .forallE _ σ τ _ := curTy | return none
+    if τ.hasLooseBVars then return none
+    unless curCL.isAppOf ``Lean.Order.instCompleteLatticePi do return none
+    let .lam _ _ τCL _ := curCL.appArg! | return none
+    let uσ ← Sym.getLevel σ
+    let uτ ← Sym.getLevel τ
+    -- `bfa : (⊥ : σ → τ) x = (⊥ : τ)`
+    let bfa := mkApp4 (mkConst ``Lean.Order.bot_apply [← decLevel uσ, ← decLevel uτ]) σ τ τCL x
+    let some (_, _, newBot) := (← Sym.inferType bfa).eq? | return none
+    -- `Eq.trans (congrFun acc x) bfa : curHead x = ⊥`
+    let cf := mkApp6 (mkConst ``congrFun [uσ, uτ]) σ (.lam `x σ τ .default) curHead curBot acc x
+    acc := mkApp6 (mkConst ``Eq.trans [uτ]) τ (mkApp curHead x) (mkApp curBot x) newBot cf bfa
+    curHead := mkApp curHead x
+    curBot := newBot
+    curTy := τ
+    curCL := τCL
+  -- `acc : rhs = ⊥`; lift through `pre ⊑ ·` and replace the target.
+  let relArgs := target.getAppArgs
+  let some α := relArgs[0]? | return none
+  let some inst := relArgs[1]? | return none
+  let some pre := relArgs[2]? | return none
+  let relPre := mkApp3 target.getAppFn α inst pre
+  let uα ← Sym.getLevel α
+  let eqProof :=
+    mkApp6 (mkConst ``congrArg [uα, .succ .zero]) α (mkSort .zero) (mkAppN head args) curBot relPre acc
+  return some (← goal.replaceTargetEq (mkApp relPre curBot) eqProof)
+
+end VCGen
+
+end Lean.Elab.Tactic.Do.Internal