rw [h_ind]
α : Type u_1
β : Type u_2
r : α → β → Prop
bs : List β
a : α
as : List α
h_ind : List.forAllRel (flip r) bs as = List.forAllRel r as bs
⊢ forAll (fun x => flip r x a) bs ∧ List.forAllRel (flip r) bs as ↔ forAll (r a) bs ∧ List.forAllRel r as bs
α : Type u_1
β : Type u_2
r : α → β → Prop
bs : List β
a : α
as : List α
h_ind : List.forAllRel (flip r) bs as = List.forAllRel r as bs
⊢ forAll (fun x => flip r x a) bs ∧ List.forAllRel r as bs ↔ forAll (r a) bs ∧ List.forAllRel r as bs