Proof by defunctionalization


Generated by why3doc 0.87.2+git