Weird proof obligations resulting from a push/pop evaluator in Coq...