Hint 2 for the math campers singing paradox

Try

cases em (∃ bob : camper, ¬ singing bob) with hyes hno,
{ cases hyes with bob key,
  use bob, },
{ push_neg at hno, -- a tactic from the glossary, which makes dealing with negations easier
  sorry, }