rw [dim_known_refines_inv Hknown Hrefines]
S : List ℕ
D : DimList
Hknown : known D = true
Hrefines : shapeRefines S D = true
⊢ project D = S
S : List ℕ
D : DimList
Hknown : known D = true
Hrefines : shapeRefines S D = true
⊢ project (List.map Dimension.Known S) = S