Theorem: List.relHead_cons_right (Algdata/Data/List/Prop.lean)

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
b : β
bs : List β
⊢ relHead r as (b :: bs) = predHead (fun a => r a b) as
Tactic:
cases as <;> rfl
State after:
no goals