{P : Sort u} →
  {m : Type → Type} →
    {t : Lean.AddMessageContext m} →
      {m' : Type → Type} →
        {t' : Lean.AddMessageContext m'} → m = m' → t ≍ t' → Lean.AddMessageContext.noConfusionType P t t'