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