Coq mechanization of the following paper: Yizhou Zhang, Andrew C. Myers. Abstraction-Safe Effect Handlers via Tunneling. Proceedings of the ACM on Programming Languages, 2(POPL), January 2019. Tested with Coq version 8.9.1.