simp_all only [and_false, or_false, and_self, or_true, not_true_eq_false, not_false_eq_true, forall_true_left,
  and_true, false_or]
case right.inl.inr.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 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
case right.inl.inr.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 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬S fst_1 fst_1