apply ih
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
h2 : hasType e τ = true
h : ∀ (x : TensorElem), x ∈ l → hasType x τ = true
⊢ hasType (nested l) τ = true
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
h2 : hasType e τ = true
h : ∀ (x : TensorElem), x ∈ l → hasType x τ = true
⊢ (List.all l fun x => hasType x τ) = true