no goals
ι : Type ?u.160749
α : Type ?u.160752
M : Type ?u.160755
N : Type ?u.160758
P : Type ?u.160761
M₀ : Type ?u.160764
G : Type ?u.160767
R : Type ?u.160770
L : List ℕ
⊢ headI L + sum (tail L) = sum L
cases L <;> simp