rw [←Hrefines.1, ←ih Hknown Hrefines.2]
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ head✝ * shapeProd tail✝ = a✝ * prod tail
no goals