∀ {C : OrderType.{u_1} → OrderType.{u_2} → Prop} (o₁ : OrderType.{u_1}) (o₂ : OrderType.{u_2}),
  (∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_2) [inst_1 : LinearOrder β],
      C (OrderType.type α) (OrderType.type β)) →
    C o₁ o₂