isElem x [] = ?isElem_rhs_1
isElem x (y :: xs) = ?isElem_rhs_3

   localZipWith f (_ :: _) (x :: ys) = ?localZipWith_rhs_1

f x :: map f xs
isElem2 x (y :: ys) with (_)
  isElem2 x (y :: ys) | with_pat = ?isElem2_rhs

  isElem3 y (y :: ys) | (Yes Refl) = ?isElem3_rhs_3

              [] => ?bar_1
              (x :: ys) => ?bar_2

elemVoid1 Here impossible
elemVoid1 (There _) impossible

                   Here impossible
                   (There _) impossible