revert head tail
l : List TensorElem
head : ℕ
tail : List ℕ
⊢ inferredShape (nested l) = some (head :: tail) →
    head = List.length l ∧ (List.all l fun x => decide (inferredShape x = some tail)) = true
l : List TensorElem
⊢ ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested l) = some (head :: tail) →
      head = List.length l ∧ (List.all l fun x => decide (inferredShape x = some tail)) = true