simp [flip]
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ ∀ {a b c : α}, flip r a b → flip r b c → flip r a c
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ ∀ {a b c : α}, r b a → r c b → r c a