simp only [prod]
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length ((x, y) :: prod [x] ys) = length [x] * length (y :: ys)