exists_elim in CPS style works but way too verbose

F* can't properly infer the implicits