∀ {lctx : Lean.LocalContext} {ctx : Lean.Expr} {lctx_1 : Lean.LocalContext} {ctx_1 : Lean.Expr},
  Lean.Elab.Term.MVarErrorKind.implicitArg lctx ctx = Lean.Elab.Term.MVarErrorKind.implicitArg lctx_1 ctx_1 →
    lctx = lctx_1 ∧ ctx = ctx_1