intros l motive_2 s H
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
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
⊢ hasShape (nested l) s = true