Used in iRevert, iClear, iFrame, and for generalizing the IH in
iInduction and iLöb.