exact MEMBER
case MEM
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ List.Mem n ?xs

case PROD
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ shapeProd ?xs > 0

case xs
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ List ℕ
case PROD
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ shapeProd shape > 0