{P : Sort u_1} →
  {α : Sort u} →
    {t : Lean.Order.CompleteLattice α} →
      {α' : Sort u} →
        {t' : Lean.Order.CompleteLattice α'} → α = α' → t ≍ t' → Lean.Order.CompleteLattice.noConfusionType P t t'