Add lemmas regarding set_seq
Adds a few potentially useful lemmas regarding set_seq
.
subset_of_set_seq
can be seen as a generalization of the existing elem_of_set_seq
. It gives equations that one can extract from knowing that one set_seq
is a subset of another set_seq
.
The lemmas subset_of_set_seq_len
and elem_of_set_seq_len
are small variants of the same lemmas without the _len
suffix. They extract information about the length or size of a set_seq
.