Remove type scope from forall notation

Closes #67

See merge request !163

Fixes #67.

notation for forall

See merge request !152

rename Z2Nat_inj_div and Z2Nat_inj_mod

See merge request !161

Revert "Merge branch 'byte-countable' into 'master'"

See merge request !160

This reverts merge request !155

Add Countable instances for byte

See merge request !155

Lemmas for `list_find` in combination with `app` and `insert`.

See merge request iris/stdpp!134

Rotate everything

See merge request iris/stdpp!136

add map_Forall_lookup

See merge request iris/stdpp!158

alternative overlay for coq/coq#12162

See merge request iris/stdpp!159

tactics.v: Fix parsing precedence for `select` tactic

See merge request iris/stdpp!157

Add Countable instance for Ascii.ascii

See merge request iris/stdpp!154

fix imap_seq and imap_seq0 to make them useful

See merge request iris/stdpp!151

Create HintDBs with the discriminated option

See merge request iris/stdpp!148

Added select and select_revert tactics

See merge request iris/stdpp!142

According to the documentation
https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:cmd.create-hintdb,
when creating a hint database without discrimination, Coq uses the
legacy implementation, which only uses Discrimination Trees for goals
without evars and does not use opaqueness information. This commit
switches the hint databases of stdpp to the new implementation.

Add filter_app lemma

See merge request iris/stdpp!147

Add `ProofIrrel ()`

See merge request iris/stdpp!146

This instance might seem odd, but `ProofIrrel` takes a `Type` and not a `Prop`,
and stdpp already has instances for products.