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

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
⊢ relHead r as [] = True
Tactic:
cases as <;> rfl
State after:
no goals