case cons e l ih =>
  simp [hasType, List.all_cons]
  intro h2 h
  simp [h2]
  apply ih
  simp[h]
  assumption
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih : (List.all l fun x => hasType x τ) = true → hasType (nested l) τ = true
⊢ (List.all (e :: l) fun x => hasType x τ) = true → hasType (nested (e :: l)) τ = true
no goals