at any moment during the development of a proof, resulting in the list
of all theorems of the library which can be applied to the current
goal. In practice, this is mostly used not really to discover what theorems
can be applied to a given goal, but to actually retrieve a theorem that
we wish to apply, but whose name we have forgotten.
at any moment during the development of a proof, resulting in the list
of all theorems of the library which can be applied to the current
goal. In practice, this is mostly used not really to discover what theorems
can be applied to a given goal, but to actually retrieve a theorem that
we wish to apply, but whose name we have forgotten.