. simp [inferredShape, H2, bind, Option.bind, H1]
case cons
head : TensorElem
s_head : ℕ
s_tail : List ℕ
H2 : inferredShape head = some s_tail
head✝ : TensorElem
tail✝ : List TensorElem
H1 : inferredShape (nested (head✝ :: tail✝)) = some (s_head :: s_tail)
⊢ inferredShape (nested (head :: head✝ :: tail✝)) = some ((s_head + 1) :: s_tail)
no goals