https://softwarefoundations.cis.upenn.edu/
http://adam.chlipala.net/cpdt/cpdt.pdf
https://proofgeneral.github.io/
proof by contradiction
https://stackoverflow.com/questions/71945260/proof-by-contradiction-in-coq
Misc. Tutorials/reference
https://cs-people.bu.edu/gaboardi/teaching/22-chalmers-course/easycrypt-refman.pdf
https://fm.csl.sri.com/SSFT23/easycrypt-tutorial.pdf
https://github.com/EasyCrypt/easycrypt
Gaboardi Course Notes, especially notes 1-11, and the second link to a lab on probabilistic noninterference.
https://cs-people.bu.edu/gaboardi/teaching/S21-CS591/
https://cs-people.bu.edu/gaboardi/teaching/S21-CS591/labs/week7/prhl-noninterference.pdf
Partial Barthe Textbook
https://software.imdea.org/~gbarthe/__introrelver.pdf
https://dl.acm.org/doi/pdf/10.1145/3290377
https://www.cs.cmu.edu/~rwh/students/tassarotti.pdf
natural deduction rules of first order logic (skalka notes)
https://ceskalka.w3.uvm.edu/misc/nd.pdf
coupling
https://arxiv.org/pdf/1509.03476.pdf
probability monads