intros h <;> induction D <;> simp
D : DimList
⊢ known D = true → shapeRefines (project D) D = true
case cons
head✝ : Dimension
tail✝ : List Dimension
tail_ih✝ : known tail✝ = true → shapeRefines (project tail✝) tail✝ = true
h : known (head✝ :: tail✝) = true
⊢ shapeRefines (project (head✝ :: tail✝)) (head✝ :: tail✝) = true