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

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