Coq mechanization of the following paper:
Yizhou Zhang and Nada Amin.
Reasoning about “Reasoning about Reasoning” Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion.
Proceedings of the ACM on Programming Languages, 6(POPL), January 2022.
Tested with Coq version 8.11.2.
The axiomatization of Lebesgue integration is based on Culpepper and Cobb.