intros h1 h2
case left
α β : 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
case left
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
h1 : S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2
h2 : 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