{D : Type u_1} →
  {Q : Type u_2} →
    {P : Sort u} →
      {left : Q → D} →
        {right : Q} →
          {left' : Q → D} →
            {right' : Q} →
              { left := left, right := right } = { left := left', right := right' } →
                (left ≍ left' → right ≍ right' → P) → P