$ ./Test id.z3-proof
SexprSxp [SexprSxp [SexprSymbol "set-logic",SexprSymbol "QF_UF"],SexprSxp [SexprSymbol "proof",SexprSxp [SexprSymbol "let",SexprSxp [SexprSxp [SexprSymbol "@x35",SexprSxp [SexprSymbol "monotonicity",SexprSxp [SexprSymbol "rewrite",SexprSxp [SexprSymbol "=",SexprSxp [SexprSymbol "=>",SexprSymbol "p",SexprSymbol "p"],SexprSymbol "true"]],SexprSxp [SexprSymbol "=",SexprSxp [SexprSymbol "not",SexprSxp [SexprSymbol "=>",SexprSymbol "p",SexprSymbol "p"]],SexprSxp [SexprSymbol "not",SexprSymbol "true"]]]]],SexprSxp [SexprSymbol "let",SexprSxp [SexprSxp [SexprSymbol "@x39",SexprSxp [SexprSymbol "trans",SexprSymbol "@x35",SexprSxp [SexprSymbol "rewrite",SexprSxp [SexprSymbol "=",SexprSxp [SexprSymbol "not",SexprSymbol "true"],SexprSymbol "false"]],SexprSxp [SexprSymbol "=",SexprSxp [SexprSymbol "not",SexprSxp [SexprSymbol "=>",SexprSymbol "p",SexprSymbol "p"]],SexprSymbol "false"]]]],SexprSxp [SexprSymbol "mp",SexprSxp [SexprSymbol "asserted",SexprSxp [SexprSymbol "not",SexprSxp [SexprSymbol "=>",SexprSymbol "p",SexprSymbol "p"]]],SexprSymbol "@x39",SexprSymbol "false"]]]]]
Have you any idea why I'm getting the above result using the version in your develop branch?