apply @TensorElem.recOn
  (motive_1 := fun e =>
    ∀s, e.inferredShape = some s → e.hasShape s)
  (motive_2 := fun l =>
    ∀s, l.all (TensorElem.inferredShape . = some s) →
      l.all (TensorElem.hasShape . s))
e : TensorElem
⊢ ∀ (shape : List ℕ), inferredShape e = some shape → hasShape e shape = true
case int
e : TensorElem
⊢ ∀ (a : ℤ) (s : List ℕ), inferredShape (int a) = some s → hasShape (int a) s = true

case float
e : TensorElem
⊢ ∀ (a : Float) (s : List ℕ), inferredShape (float a) = some s → hasShape (float a) s = true

case bool
e : TensorElem
⊢ ∀ (a : Bool) (s : List ℕ), inferredShape (bool a) = some s → hasShape (bool a) s = true

case nested
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

case empty
e : TensorElem
⊢ ∀ (s : List ℕ), inferredShape empty = some s → hasShape empty s = true

case nil
e : TensorElem
⊢ ∀ (s : List ℕ),
    (List.all [] fun x => decide (inferredShape x = some s)) = true → (List.all [] fun x => hasShape x s) = true

case cons
e : TensorElem
⊢ ∀ (head : TensorElem) (tail : List TensorElem),
    (∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true) →
      (∀ (s : List ℕ),
          (List.all tail fun x => decide (inferredShape x = some s)) = true →
            (List.all tail fun x => hasShape x s) = true) →
        ∀ (s : List ℕ),
          (List.all (head :: tail) fun x => decide (inferredShape x = some s)) = true →
            (List.all (head :: tail) fun x => hasShape x s) = true