Hint 1 for the math campers singing paradox

Try

cases em (∃ bob : camper, ¬ singing bob) with hyes hno,
{ cases hyes with bob key,
  sorry, },
{ sorry, }

Need more hints?