for H being ZF-formula
for x, y being Variable st not x in variables_in H holds
H / (x,y) = H