∀ {δ : Sort u_3} (f : (α : Type u_1) → [LinearOrder α] → (β : Type u_2) → [LinearOrder β] → δ),
  (∀ (α₁ : Type u_1) [inst : LinearOrder α₁] (β₁ : Type u_2) [inst_1 : LinearOrder β₁] (α₂ : Type u_1)
      [inst_2 : LinearOrder α₂] (β₂ : Type u_2) [inst_3 : LinearOrder β₂],
      OrderType.type α₁ = OrderType.type α₂ → OrderType.type β₁ = OrderType.type β₂ → f α₁ β₁ = f α₂ β₂) →
    ∀ (w₁ : LinOrd) (w₂ : LinOrd) (v₁ : LinOrd) (v₂ : LinOrd), w₁ ≈ v₁ → w₂ ≈ v₂ → f ↑w₁ ↑w₂ = f ↑v₁ ↑v₂