simp [List.forAllRel, map, cons_bind, List.forAll]
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
bs : List β
⊢ List.forAllRel r (a :: as) bs = (forAll (r a) bs ∧ List.forAllRel r as bs)
no goals