injectivity_store : (string * thm) list ref

SYNOPSIS: Internal theorem list of injectivity theorems.
DESCRIPTION: This list contains all the injectivity theorems (see injectivity) for the recursive types defined so far. It is automatically extended by define_type and used as a cache by injectivity.
FAILURE CONDITIONS: Not applicable.
SEE ALSO: define_type, distinctness_store, extend_rectype_net, injectivity.