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:
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.