induction as
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
b : β
bs : List β
⊢ List.forAllRel r as (b :: bs) = (forAll (fun x => r x b) as ∧ List.forAllRel r as bs)
case nil
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
⊢ List.forAllRel r [] (b :: bs) = (forAll (fun x => r x b) [] ∧ List.forAllRel r [] bs)

case cons
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
head✝ : α
tail✝ : List α
tail_ih✝ : List.forAllRel r tail✝ (b :: bs) = (forAll (fun x => r x b) tail✝ ∧ List.forAllRel r tail✝ bs)
⊢ List.forAllRel r (head✝ :: tail✝) (b :: bs) =
    (forAll (fun x => r x b) (head✝ :: tail✝) ∧ List.forAllRel r (head✝ :: tail✝) bs)