There is an unsaved comment in progress. You will lose your changes if you continue. Are you sure you want to reopen the work item?
Erroneous encoding of hypotheses involving primed variables
Sequents that have VARIABLE parameters, which occur primed in the hypotheses are translated inconsistently for the backends, making it impossible to apply them to prove anything. A minimal example is attached.
If you look at the input files produced for the different backends, the primed variable is called (something like) var' in some places and var_hash_prime in others.