intros Hknown
D : DimList
S : List ℕ
⊢ known D = true → shapeRefines S D = true → D = List.map Dimension.Known S
D : DimList
S : List ℕ
Hknown : known D = true
⊢ shapeRefines S D = true → D = List.map Dimension.Known S