Rename existing asymmetric lemma `singleton_included` into `singleton_included_l`.

add OFE structure for Prop

See merge request iris/iris!418

Remove namespaces from lock API.

See merge request iris/iris!416

Better proof mode support for telescope + add missing BI instances

See merge request iris/iris!415

Also make better use of `Implicit Types` and group instances better.

Notion of composition on `oFunctor`s, and some renaming

See merge request iris/iris!411

`{o,r,ur}Functor_map_{ne,id,compose,contractive}`.

Make `_iff` and `_alter` lemmas for invariants consistent, and add `_iff` lemma for locks

See merge request iris/iris!414

They follow the pattern of `wp_wand`.

Kill `{o,r,ur}Functor_diag` coercions, and rename into `{o,r,ur}Functor_apply`

Closes #240

See merge request iris/iris!413

Add notion of isomorphism between OFEs

See merge request iris/iris!410