{α : Sort u_1} →
  {β : Sort u_2} →
    {γ : Sort u_3} →
      {r : α → β → Sort u} →
        {s : β → γ → Sort v} →
          {t : outParam (α → γ → Sort w)} →
            {P : Sort u_4} →
              {trans trans' : {a : α} → {b : β} → {c : γ} → r a b → s b c → t a c} →
                { trans := trans } = { trans := trans' } → (trans ≍ trans' → P) → P