∀ (f fType : Lean.Expr) (args : List Lean.Elab.Term.Arg) (namedArgs : List Lean.Elab.Term.NamedArg)
  (expectedType? : Option Lean.Expr) (etaArgs : Array (Lean.Name × Lean.Expr))
  (toSetErrorCtx instMVars : Array Lean.MVarId) (propagateExpected : Bool) (resultTypeOutParam? : Option Lean.MVarId)
  (foundNamedArgs : Array Lean.Name) (f_1 fType_1 : Lean.Expr) (args_1 : List Lean.Elab.Term.Arg)
  (namedArgs_1 : List Lean.Elab.Term.NamedArg) (expectedType?_1 : Option Lean.Expr)
  (etaArgs_1 : Array (Lean.Name × Lean.Expr)) (toSetErrorCtx_1 instMVars_1 : Array Lean.MVarId)
  (propagateExpected_1 : Bool) (resultTypeOutParam?_1 : Option Lean.MVarId) (foundNamedArgs_1 : Array Lean.Name),
  ({ f := f, fType := fType, args := args, namedArgs := namedArgs, expectedType? := expectedType?, etaArgs := etaArgs,
        toSetErrorCtx := toSetErrorCtx, instMVars := instMVars, propagateExpected := propagateExpected,
        resultTypeOutParam? := resultTypeOutParam?, foundNamedArgs := foundNamedArgs } =
      { f := f_1, fType := fType_1, args := args_1, namedArgs := namedArgs_1, expectedType? := expectedType?_1,
        etaArgs := etaArgs_1, toSetErrorCtx := toSetErrorCtx_1, instMVars := instMVars_1,
        propagateExpected := propagateExpected_1, resultTypeOutParam? := resultTypeOutParam?_1,
        foundNamedArgs := foundNamedArgs_1 }) =
    (f = f_1 ∧
      fType = fType_1 ∧
        args = args_1 ∧
          namedArgs = namedArgs_1 ∧
            expectedType? = expectedType?_1 ∧
              etaArgs = etaArgs_1 ∧
                toSetErrorCtx = toSetErrorCtx_1 ∧
                  instMVars = instMVars_1 ∧
                    propagateExpected = propagateExpected_1 ∧
                      resultTypeOutParam? = resultTypeOutParam?_1 ∧ foundNamedArgs = foundNamedArgs_1)