rw [List.forAllRel_cons_left] at this
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
this : List.forAllRel r (a :: as) bs
⊢ forAll (r a) bs
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
this : forAll (r a) bs ∧ List.forAllRel r as bs
⊢ forAll (r a) bs