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

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

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