revert S
S : List ℕ
D : DimList
Hknown : known D = true
⊢ shapeRefines S D = true → shapeProd S = prod D
D : DimList
Hknown : known D = true
⊢ ∀ {S : List ℕ}, shapeRefines S D = true → shapeProd S = prod D