[ fix ] rewriting the search procedure

I think I have finally found a good way to represent the proof search
process: assuming that CON is the context of consumption-annotated
resources and that G is the goal to be discharged, we describe the
proof search problem as follow (? stand for values to be determined):

           ?
CON => -----------
        ? |- G

When we find a rule which can be applied, CON is (if needed)
destructively updated to record the consumption of resources
implied by this rule:

            ?                               proof
CON => ----------  -^v^v-> CON \ VAL => ------------ rule
        ? |- G                            VAL |- G