distinctness_store : (string * thm) list ref

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