Educational Pearl: 'Proof-directed debugging' revisited for a first-order version