{m : Type u_1 → Type u_2} →
  {P : Sort u} →
    {toAlternative : Alternative m} →
      {toBind : Bind m} →
        {toAlternative' : Alternative m} →
          {toBind' : Bind m} →
            { toAlternative := toAlternative, toBind := toBind } =
                { toAlternative := toAlternative', toBind := toBind' } →
              (toAlternative ≍ toAlternative' → toBind ≍ toBind' → P) → P