Add `encode_Z` function to encode element of countable type as `Z`.

See merge request iris/stdpp!145

Another try at removing strings.length

See merge request iris/stdpp!144

Add tests for equiv notation

See merge request iris/stdpp!143

Extracted from iris!409.

Add notation `wn` of weakly normalizing terms; and prove some common theorems about it.

See merge request !140

Revise uses of inj as discussed

See merge request !138

Code not affected by a00d9bd8.

All occurrences are gone, except for one in `base.v` where you'd need different
functions.

However, I'm unsure this is an improvement: in lots of cases here, the function
didn't need to be guessed, but could be deduced by "simple" higher-order
unification, the one where unifying `?f ?a` against `g args last_arg` sets `?f =
g args`.

Code affected by a00d9bd8.

Rename `fin_maps.singleton_proper` into `singletonM_proper`.

See merge request iris/stdpp!137

add sed script for 1.3.0

See merge request !128

Fix typo in CHANGELOG

See merge request !135

Rename performed in !131 was on drop_insert, not drop_length

random collection of lemmas

See merge request !131

Remove trailing whitespace

See merge request !133

This was done using `sed --in-place 's/[[:space:]]\+$//' theories/*.v`.

Replace explicit use of Inj instances by inj

See merge request !132

This was inconsistent and not explained before.