exact hT2.left hT1
case inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hT1 : T p.2 p.2
hT2 : ¬T p.2 p.2 ∧ ¬T p.2 p.2 ∧ p.2 = p.2
⊢ False
no goals