rcases hS.trich p.1 p.1 with (hS2 | hS3 | hS4)
case 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 : α × β
hS1 : S p.1 p.1
⊢ False
case inl.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 : α × β
hS1 : S p.1 p.1
hS2 : ¬S p.1 p.1 ∧ ¬S p.1 p.1 ∧ p.1 = p.1
⊢ False

case inl.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 : α × β
hS1 : S p.1 p.1
hS3 : ¬S p.1 p.1 ∧ S p.1 p.1 ∧ ¬p.1 = p.1
⊢ False

case inl.inr.inr
α β : 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 : α × β
hS1 : S p.1 p.1
hS4 : S p.1 p.1 ∧ ¬S p.1 p.1 ∧ ¬p.1 = p.1
⊢ False