intros Hknown Hrefines
S : List ℕ
D : DimList
⊢ known D = true → shapeRefines S D = true → project D = S
S : List ℕ
D : DimList
Hknown : known D = true
Hrefines : shapeRefines S D = true
⊢ project D = S