ifp-proofs Formal verification code for IFP In IFP.lean, Veil does not generate counterexamples with set_option veil.printCounterexamples true. In IFP2.lean also, the above issue occurs.