Problem 96 "Principle of Inclusion/Exclusion" of 100 on this list now has a formalisation (pdf) and proof.