We need to document how to use this kind of proof
We need to document how to use this kind of proof