induction D <;> intros S Hrefines <;> simp
D : DimList
Hknown : known D = true
⊢ ∀ {S : List ℕ}, shapeRefines S D = true → shapeProd S = prod D
case nil
Hknown : known [] = true
S : List ℕ
Hrefines : shapeRefines S [] = true
⊢ shapeProd S = 1

case cons
head✝ : Dimension
tail✝ : List Dimension
tail_ih✝ : known tail✝ = true → ∀ {S : List ℕ}, shapeRefines S tail✝ = true → shapeProd S = prod tail✝
Hknown : known (head✝ :: tail✝) = true
S : List ℕ
Hrefines : shapeRefines S (head✝ :: tail✝) = true
⊢ shapeProd S = prod (head✝ :: tail✝)