{P : Sort u} →
  {eager : Lean.Lsp.CodeAction} →
    {lazy? : Option (IO Lean.Lsp.CodeAction)} →
      {eager' : Lean.Lsp.CodeAction} →
        {lazy?' : Option (IO Lean.Lsp.CodeAction)} →
          { eager := eager, lazy? := lazy? } = { eager := eager', lazy? := lazy?' } →
            (eager = eager' → lazy? = lazy?' → P) → P