Sounds like a homework question! You need to skolemize s, then expose its associated type predicate, expand the definition of even?, and it should be obvious from there on. Good luck, John