Add some useful advantage properties

[cmester0]

No description provided.

[cmester0]

@MarkusKL @spitters These statements should hopefully enable simpler proof structure and thus better automation. We seem to be missing some weakening statement, as ValidPackage now requires the export interface to match exactly.

[MarkusKL]

To resolve.

[MarkusKL]

You may be able to use id_link to explicitly remove functions from a package. Previously, I have also found a lemma like this useful: P o ID I o P' = P o P' where imports of P are a submap of I, which is a submap of the exports of P'.

[cmester0]

I made a valid version of the weakening statement. But if we force E to be the export interface of p, then we could just drop E?

[MarkusKL]

I do not understand what you need the weakening lemma for, so I cannot say if it is on the right form. Does it apply to any of the examples in this repository?

[spitters]

Should be revisited after nominal:
#82

[4ever2]

I rebased this on top of the nominal changes.

@MarkusKL most of your comments were addressed. Is there anything more blocking this from being merged?