no goals
ι : Type ?u.69762
α : Type ?u.69765
M : Type u_1
N : Type ?u.69771
P : Type ?u.69774
M₀ : Type ?u.69777
G : Type ?u.69780
R : Type ?u.69783
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝ : Inhabited M
l : List M
h : l ≠ []
⊢ headI l * prod (tail l) = prod l
cases l <;> [contradiction; simp]