unfold length
α : 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)
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length (prod [x] ys) + 1 = (length [] + 1) * (length ys + 1)