When analysing / describing proofs, as well as when explaining the complexity of a particular schema/lemma/proof, it's often useful to know the number of terms / bindings / predicates / invariants /expressions involved. Counting the kind of terms involved should be trivial by traversing the AST for the right type. The bindings of a schema are trickier, yet solved by the definition table within the VCG. It would be nice to have the ability to display them within the eclipse environment.