simp_arith
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
s_head' : ℕ
s_tail' : List ℕ
Heq : head_shape = s_tail'
H : s_head' + 1 = s_head
H' : s_tail' = s_tail
⊢ 0 < s_head' + 1
no goals