Add lemmas `app_cons_eq_inv_{l,r}`.

See merge request iris/stdpp!363

Add `last_cons_Some_ne` lemma for the `last` function

See merge request iris/stdpp!361

Added some useful lemmas about [list_subseteq]

See merge request iris/stdpp!359

Set the priority of the rewrite relation for sqsubseteq to not take precedence over...

See merge request iris/stdpp!362

Add lemmas about empty `filter` on list, map, and set

See merge request iris/stdpp!358

Set the priority of the rewrite relation for equiv to not take precedence over...

See merge request iris/stdpp!360

Add lemmas `elem_of_prefix` and `elem_of_suffix`

See merge request iris/stdpp!354

Added some useful lemmas for the [last] function

See merge request iris/stdpp!355

Declare `equiv` as a rightful rewrite relation, when an `Equiv` instance is available.

See merge request iris/stdpp!273

add some lemmas about `Finite` and `pred_finite`

See merge request iris/stdpp!351

Also, rename `dec_pred_finite{,_set}` to `dec_pred_finite{,_set}_alt`.

Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.

See merge request iris/stdpp!352

remove a Global Arguments Pos.of_nat from the middle of a proof

See merge request iris/stdpp!350