aesop_subst a
case right.inr.inl.inr
α β : 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 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
a : fst_1 = fst
⊢ ¬T snd_1 snd_1
case right.inr.inl.inr
α β : 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 snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst ∧ ¬S fst fst ∧ ¬fst = fst
⊢ ¬T snd_1 snd_1