dsimp [List.forAllRel, forAll] at *
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
h_ind : List.forAllRel r as [] = True
⊢ List.forAllRel r (a :: as) [] = True
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
h_ind : forAll (fun a => True) as = True
⊢ (True ∧ forAll (fun a => True) as) = True