Add function to get list of global identifiers
Add function to count how many new metavariables should be generated to reify a proof state