induction MEM
xs : List ℕ
x : ℕ
MEM : List.Mem x xs
⊢ shapeProd xs > 0 → x > 0
case head
xs : List ℕ
x : ℕ
as✝ : List ℕ
⊢ shapeProd (x :: as✝) > 0 → x > 0

case tail
xs : List ℕ
x b✝ : ℕ
as✝ : List ℕ
a✝ : List.Mem x as✝
a_ih✝ : shapeProd as✝ > 0 → x > 0
⊢ shapeProd (b✝ :: as✝) > 0 → x > 0