Inclusion i
or
where either types T and 
are equivalent or T is a proper subtype
of 
. The specific kinds of relations between T and 
that the
Inclusion currently handles are roughly:
are the same once all soft abstractions are unfolded
are both universe or prop terms and the level of T is
always no greater than the level of 
for any instantiation of level
variables.
are each formed by using one or more subset types,
and both have some common superset type. In this case Inclusion
tries to show that the subset predicates (if any) of 
are implied
by the subset predicates (if any) of T together with other hypotheses.
have the same outermost type constructor. In this
case, the inclusion goal is reduced to one or more inclusion
goals involving the immediate subterms of T and 
. Currently works
for function, product, union and list types.
.
Inclusion also solves similar goals where one or both of the membership terms are replaced by equality terms.
For the inclusion reasoning involving subset types to work, you need to supply information about abstractions involving subset types using the function add_set_inclusion_info. See the theory int_1 for several examples of the use of this function.