-results required for proving P, prefixed by simple modalities (<,@,...) explaining
-the way the result is used (e.g. for rewriting, in an applicative step, and so on).
+objects involved in the proof, prefixed by simple modalities (#,<,@,...) explaining
+the way it is actually used (e.g. for introduction, rewriting, in an applicative
+step, and so on).