Skip to content

Stronger sorted unique lemmas

Robbert Krebbers requested to merge robbert/sorted_unique into master

Add lemmas Sorted_unique' and StronglySorted_unique' that only require anti symmetry for the elements that are in the list.

Merge request reports