WIP: Interpretation of πDILL

Hi, I would like to request comments on something that I've been working on.

πDILL is a type system based on intuitionistic linear logic, formulated in the dual context-style: https://doi.org/10.1017/S0960129514000218

In this PR I tried to write down the interpretation for this system using heap_lang (instead of pi-calculus), and interpret the types with Actris channels.

Why I thought this might be interesting?

• I wanted to learn Actris
• The type system fundamentally requires higher-order channels (something that is well supported in Actris)
• It shows an example of "non-manifest" sharing, where one endpoint (a "server") is shared among clients, but all the client-server interactions are totally disjoint from each other.

Overview of changes in this PR:

• Some facts about substitutions; the is_closed_expr_set was taken from ReLoC.
• A lemma about big_sepM2.
• In order to implement this "non-manifest sharing" (for the interpretation of ! A types) I had to tweak the iProto_owns definition and formulate a log-atomic style specifications for the send operation.

I think the first two items are orthogonal to Actris/DILL so it might sense to see if those results can be generalized and move upstream.