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