case nested =>
  intros l motive_2 s Hshape Htype
  cases s <;> simp [hasShape] at Hshape
  case cons s_head s_tail =>
  simp [TensorElem.flatten_list, shapeProd, List.foldr]
  simp [motive_2 s_tail Hshape.2 (hasType_list_1 Htype)]
  simp [shapeProd, Nat.mul_comm, Hshape.1]
τ : MLIRTy
⊢ ∀ (a : List TensorElem),
    (∀ (s : List ℕ),
        (∀ (x : TensorElem), x ∈ a → hasShape x s = true) →
          ∀ (h : (List.all a fun x => hasType x τ) = true),
            List.length (List.join (mapWithType a flatten (_ : hasType (nested a) τ = true))) =
              List.length a * shapeProd s) →
      ∀ (s : List ℕ),
        hasShape (nested a) s = true →
          ∀ (h : hasType (nested a) τ = true), List.length (flatten (nested a) h) = shapeProd s
no goals