∀ (preContext : Lean.Meta.AC.PreContext) (atoms : Array Lean.Expr)
  (k : Array (Lean.Expr × Option Lean.Expr) → Lean.MetaM Lean.Expr) (α : Lean.Expr) (u : Lean.Level) (i : ℕ)
  (acc : Array (Lean.Expr × Option Lean.Expr)) (vars args : Array Lean.Expr),
  Lean.Meta.AC.abstractAtoms.go✝ preContext atoms k α u i acc vars args =
    if h : i < atoms.size then
      Lean.Meta.withLocalDeclD `x α fun v => do
        let __do_lift ← Lean.Meta.AC.getInstance `Std.LawfulIdentity #[preContext.op, atoms[i]]
        match __do_lift with
          | none =>
            Lean.Meta.AC.abstractAtoms.go✝¹ preContext atoms k α u (i + 1) (acc.push (v, none)) (vars.push v)
              (args.push atoms[i])
          | some inst =>
            Lean.Meta.withLocalDeclD `inst (Lean.mkApp3 (Lean.mkConst `Std.LawfulIdentity [u]) α preContext.op v)
              fun iv =>
              Lean.Meta.AC.abstractAtoms.go✝² preContext atoms k α u (i + 1) (acc.push (v, some iv)) (vars ++ #[v, iv])
                (args ++ #[atoms[i], inst])
    else do
      let proof ← k acc
      let proof ← Lean.Meta.mkLambdaFVars vars proof
      have proof : Lean.Expr := Lean.mkAppN proof args
      pure proof