{P : Sort u_1} →
  {α : Type u} →
    {t : Std.Packages.LinearOrderOfLEArgs α} →
      {α' : Type u} →
        {t' : Std.Packages.LinearOrderOfLEArgs α'} →
          α = α' → t ≍ t' → Std.Packages.LinearOrderOfLEArgs.noConfusionType P t t'