This PR initializes some documentation for our proofs. It adds some almost empty files and makes sure that we can show documentation for the PfRule enum.
Kind