conv =>
  lhs
  rw [←and_assoc (c:=List.forAllRel _ _ _), and_assoc (a:=r a b), And.comm (a:=List.forAll _ _) (b:=List.forAll _ _), ←and_assoc]
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
a : α
as : List α
h_ind : List.forAllRel r as (b :: bs) = (forAll (fun x => r x b) as ∧ List.forAllRel r as bs)
⊢ ((r a b ∧ forAll (r a) bs) ∧ forAll (fun x => r x b) as ∧ List.forAllRel r as bs) =
    ((r a b ∧ forAll (fun x => r x b) as) ∧ List.forAllRel r (a :: as) bs)
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
a : α
as : List α
h_ind : List.forAllRel r as (b :: bs) = (forAll (fun x => r x b) as ∧ List.forAllRel r as bs)
⊢ (((r a b ∧ forAll (fun x => r x b) as) ∧ forAll (r a) bs) ∧ List.forAllRel r as bs) =
    ((r a b ∧ forAll (fun x => r x b) as) ∧ List.forAllRel r (a :: as) bs)