Helper method for creating auxiliary lemmas in the environment.
It uses a cache that maps
type to declaration name. The cache is not stored in
It is useful to make sure the same auxiliary lemma is not created over and over again in the same file.
This method is useful for tactics (e.g.,
simp) that may perform preprocessing steps to lemmas provided by
users. For example,
simp preprocessor may convert a lemma into multiple ones.