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

State before:
α : Type
inst✝ : Inhabited α
xs : List α
⊢ head [head xs] = head xs
Tactic:
cases xs with
| nil        => rfl
| cons x xs' => rfl
State after:
no goals

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

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