Given an inductive definition of a type *I*, one can exploit its
generated elimination principle to define functions with domain *I*.
The range of such a definition is limited by the universe of the
elimination principle i.e., `Prop`, `Type(i)` or
`Type`. Recall that `Prop` `Type(i)` `Type`. Hence, the theories
of inductive definition vary according to the choice of universe. In
particular, one cannot prove disjointness of constructors for any
inductive definition which is eliminated over the kind `Prop`.

The environmental variable `LEGOPATH` controls the search path
for LEGO modules. By default it accommodates elimination over
`Type` and inductive types inhabiting `Type`. It is set to
`.:$LIBDIR/lib_Type:$LIBDIR` where `LIBDIR` records
the root directory of the library.

Users who prefer elimination over

`Prop`- need to replace
`lib_Type`by`lib_Prop`in their`LEGOPATH`. In this configuration, inductive types inhabit the kind`Prop`. `Type(2)`- need to replace
`lib_Type`by`lib_TYPE`in their`LEGOPATH`. In this configuration, inductive types inhabit the kind`Type(0)`

- their
`LEGOPATH`considers their version of`parameters`before any such module in the library -
`LEGOPATH`has to include`lib_TYPE`.