Skip to content

Add lemmas regarding set_seq

Simon Friis Vindum requested to merge simonfv/stdpp:set-seq-lemmas into master

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.

Merge request reports