case nested =>
  intros l motive_2 s H
  let H' := inferredShape_list_to_cons H
  cases H'; case intro s_tail Hs =>
    rw [Hs]; rw [Hs] at H; clear Hs H'
    let H' := inferredShape_list H
    simp [hasShape, motive_2 _ H'.2]
e : TensorElem
⊢ ∀ (a : List TensorElem),
    (∀ (s : List ℕ),
        (List.all a fun x => decide (inferredShape x = some s)) = true → (List.all a fun x => hasShape x s) = true) →
      ∀ (s : List ℕ), inferredShape (nested a) = some s → hasShape (nested a) s = true
no goals