{P : Sort u} →
  {lctx : Lean.LocalContext} →
    {ctx : Lean.Expr} →
      {lctx' : Lean.LocalContext} →
        {ctx' : Lean.Expr} →
          Lean.Elab.Term.MVarErrorKind.implicitArg lctx ctx = Lean.Elab.Term.MVarErrorKind.implicitArg lctx' ctx' →
            (lctx = lctx' → ctx = ctx' → P) → P