{P : Sort u} →
  {ε α : Type} →
    {t : Lean.ExceptToEmoji ε α} →
      {ε' α' : Type} →
        {t' : Lean.ExceptToEmoji ε' α'} → ε = ε' → α = α' → t ≍ t' → Lean.ExceptToEmoji.noConfusionType P t t'