cases τ <;> simp [hasType] at Htype
τ : MLIRTy
i : ℤ
s : List ℕ
Hshape : hasShape (int i) s = true
Htype : hasType (int i) τ = true
⊢ List.length (flatten (int i) Htype) = shapeProd s
case int
i : ℤ
s : List ℕ
Hshape : hasShape (int i) s = true
a✝¹ : Signedness
a✝ : ℕ
Htype✝ : hasType (int i) (MLIRType.int a✝¹ a✝) = true
Htype : FinInt.isInBounds a✝¹ a✝ i = true
⊢ List.length (flatten (int i) Htype✝) = shapeProd s