Coq formalization of the work in my dissertation. Tested to work with Coq 8.19.1, coq-itree 5.2.0, and coq-paco 4.2.0.