We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
:ctf- { eq [ <label-exp> ] <term> = <term> .}
Like :ctf, but if sub-goals are not discharged, the CITP prover returns to the original state before the reduce action.
:ctf
Related: :ctf, citp
citp