rw [←forAllRel_flip, ←forAllRel_flip (r:=r)]
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
bs : List β
⊢ List.forAllRel r as (reverse bs) = List.forAllRel r as bs
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
bs : List β
⊢ List.forAllRel (flip r) (reverse bs) as = List.forAllRel (flip r) bs as