Generalize wp_lb_init to steps_lb_0.

See merge request iris/iris!1022

egrep -> grep -E

See merge request iris/iris!1019

Add laws to allow "undiscarding" points-tos

See merge request iris/iris!960

Remove needless later in total adequacy.

See merge request iris/iris!1018

rename head_step → base_step

See merge request !1012

rename mapsto → pointsto

Closes #495

See merge request !1013

Tweak lemmas for discrete and total `cmra_update`

See merge request !1016

`cmra_discrete_updateP` → `cmra_discrete_total_updateP`; repurpose
existing lemmas for version with only `CmraDiscrete`.

Fixed iFrame under ∧ and ∨ taking forever to fail in the presence of evars

See merge request !989

Adapt to https://github.com/coq/coq/pull/14928

See merge request !1015

Followup for !1011

See merge request !1014