{α : Type u_3} →
  {P : Sort u} →
    {toProd : α × α} →
      {fst_ne_snd : toProd.1 ≠ toProd.2} →
        {toProd' : α × α} →
          {fst_ne_snd' : toProd'.1 ≠ toProd'.2} →
            { toProd := toProd, fst_ne_snd := fst_ne_snd } = { toProd := toProd', fst_ne_snd := fst_ne_snd' } →
              (toProd ≍ toProd' → P) → P