termination does not automatically prove equivariance for the defined function (label: no_eqvt)

use_thys ["Paper"];