Really, *all* of our files contain proof rules