Case expressions at the root of a definition should contribute to termination

[janmasrovira]

E.g. it should be possible to write

isMember {A} (testEq : A → A → Bool) (element : A) (list : List A) : Bool := case list of {
  | nil := false
  | x :: xs := testEq element x || isMember testEq element xs 
};

Moreover, we'd like to support simultaneously casing on multiple elements with the help of the Pair type (or any other product type) and still detect termination.

zipWith {A B C} (f : A -> B -> C) (list1 : List A) (list2 : List B) : List C := case list1, list2 of {
  | nil, _ := nil
  | _, nil := nil
  | x :: xs, y :: ys := f x y :: zipWith f xs ys
};