Also weaken some specs by adding laters.

- Allow for binders in protocols.
- Model protocols in CPS style using the COFE solver.
- Change the channel methods so they do not mention sides.
- Lots of refactoring.
- Generalize the `list_sort` example.
- Move stuff to stdpp/Iris.

Maintaining the same example twice is just too much work.

- Put code and proofs of examples in a single file.
- Rename encode/decode to avoid conflicts with encode/decode (of the countable class) in stdpp.
- Remove useless imports.

commit a96494d62639ca14449d90c3a510c3a63a28fc07
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Tue May 7 18:39:41 2019 +0200

    Finalized List sort example, and introduced list encodings

commit 1b9fc4de897a5ea15c0e9a11b4ace407adda02ad
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Fri May 3 15:28:21 2019 +0200

    WIP List sort example

commit 4ce5eb98585f25daa6b5682cdc6ab34a192f2b69
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Fri May 3 11:18:07 2019 +0200

    WIP list sort example

Squashed commit of the following:

commit b404feb30cecf7678c0ad6007171a13361483086
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Wed Apr 17 17:36:21 2019 +0200

    Bumped try_recv and recv to ofe st's

commit 4aa2399d02de67feacdcba9d0929cd7e20a1f7da
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Wed Apr 17 15:19:14 2019 +0200

    Finalised send proof

commit ae9857fcf8a88e917b6ccb219ac6e27a1afe46e2
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date:   Wed Apr 17 14:58:34 2019 +0200

    Tweak.

commit 4d86571d9d51992d6ee83fdfbbfbec24ce8fdbc8
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date:   Wed Apr 17 14:54:44 2019 +0200

    Work.

commit 0fedd453c2ce41862f0a2040294ad0d271e39e85
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Wed Apr 17 12:55:52 2019 +0200

    Bumped Robbert feedback, WIP send st triple

commit f5672f9a529699ca0610329d32c59ad33d3146de
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Tue Apr 16 14:43:52 2019 +0200

    WIP

commit ef354c3899e796ccb091e1275e8b44d12a3393fd
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Tue Apr 16 13:39:41 2019 +0200

    Lifted stype over OFEs. Fixed residuals in channel.v

commit 1a47979d7497adb8c14ac9b57caf5632383ef2c3
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Tue Apr 16 13:08:28 2019 +0200

    WIP

commit 605562ba86b9481ae367409c87492b61d199111f
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Tue Apr 16 13:05:03 2019 +0200

    Test

commit 77eb6feb071da540fbc424602628c045ea15c004
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date:   Mon Apr 15 16:24:13 2019 +0200

    Working.

Made initial definition of session type allocation on new channel creation.

Generalized buffer CMRA to work for any type.

Introduced Authoritative Exclusive buffer CMRA.