induction S <;> simp
S : List ℕ
⊢ project (List.map Dimension.Known S) = S
case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : project (List.map Dimension.Known tail✝) = tail✝
⊢ project (List.map Dimension.Known tail✝) = tail✝