simp_rw [R5]
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
⊢ (R5 S T p q → R5 S T q j → R5 S T p j) ∧ Trichotomy (R5 S T p q) (R5 S T q p) (p = q)
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
⊢ (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2 → S q.1 j.1 ∨ q.1 = j.1 ∧ T q.2 j.2 → S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2) ∧
    Trichotomy (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) (p = q)