Net of injectivity and distinctness properties for recursive type constructors.
DESCRIPTION
HOL Light maintains a net of theorems used to simplify equations between
elements of recursive datatypes; essentially these include injectivity and
distinctness, e.g. CONS_11 and NOT_CONS_NIL for lists. This net is used in
some situations where such things need to be proved automatically, notably in
define. A call to basic_rectype_net() returns that net. It is automatically
updated whenever a type is defined by define_type.