revert shape
τ : MLIRTy
e : TensorElem
shape : List ℕ
⊢ hasShape e shape = true → ∀ (h : hasType e τ = true), List.length (flatten e h) = shapeProd shape
τ : MLIRTy
e : TensorElem
⊢ ∀ (shape : List ℕ), hasShape e shape = true → ∀ (h : hasType e τ = true), List.length (flatten e h) = shapeProd shape