The 'clause_aux' function backchains G in {L |- G} on some clause in
L or in the program. It never uses the hypotheses.