gmap_view: add deletion lemma

See merge request iris/iris!541

Make `solve_inG` faster.

See merge request iris/iris!532

1.) First `simpl` away all the functors 2.) Don't use `done`, which calls `split`.

add a general gmap_view library and use it for wsat, gen_heap, proph_map

Closes #328

See merge request iris/iris!486

fix combining two q/2 fractions to a q

See merge request iris/iris!540

generalize dfrac IsOp instance

See merge request iris/iris!537

prove a funny consequence of Löb induction

See merge request iris/iris!538

Counterexamples for affine+em and Löb+em.

See merge request iris/iris!536

Consistent naming for auth/view lemmas.

See merge request iris/iris!533

add iff lemma for '✓ (to_agree a ⋅ to_agree b)'

See merge request iris/iris!535

Also rename the recently added `view_update_alloc_frac` into
`view_update_frac_alloc` to be consistent with other lemmas about the
placement of `_frac`.

Use infix `_frac` for the `●{q}` variants. This was already done for the
external validity lemmas, but not for those for inclusion and internal validity.

dfrac: do not track discarded fraction

See merge request iris/iris!531

Put `iProp`/`iPreProp`-isomorphism into `own` construction

See merge request iris/iris!530