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

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