A parameter has disappeared during a refinement. If this is intentional, add a witness (3.2.3.4.4) to tell the machine how the abstract parameter should refined.