This is a pair consisting of an empty list of terms and a null instantiation
(see null_inst). It is used inside most tactics to indicate that they do
nothing interesting with metavariables.
FAILURE CONDITIONS
Not applicable.
COMMENTS
This is not intended for general use, but readers writing custom tactics from
scratch may find it convenient.