aesop_subst [right, right_2]
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : ¬T snd_1 snd
right : snd = snd_1
⊢ ¬(S fst_1 fst_1 ∨ T snd_1 snd_1)
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left_1 left_3 : ¬T snd_1 snd_1
left left_2 : ¬S fst_1 fst_1
⊢ ¬(S fst_1 fst_1 ∨ T snd_1 snd_1)