Theorem: LoVe.head_head (LoVe/Lectures/LoVe05_FunctionalProgramming_Demo.lean)

State before:
α : Type
inst✝ : Inhabited α
xs : List α
⊢ head [head xs] = head xs
Tactic:
rfl
State after:
no goals