{motive : Lean.Elab.Tactic.Do.VCGen.Result → Sort u} →
  (t : Lean.Elab.Tactic.Do.VCGen.Result) →
    ((invariants vcs : Array Lean.MVarId) → motive { invariants := invariants, vcs := vcs }) → motive t