Propositional subtyping should consider the lexical type environment

Problem

Subtyping between propositions could be improved, especially when mixing positive and
negative type propositions.

Take the following function.

The subtyping test for the {then} proposition fails because

is not a subtype of

However in the context of the current lexical environment,

combined with the actual then proposition

implies

.

Approach

Every {FilterSet} should also carry the {PropEnv} in which it was created. (We should take care that this
environment is substituted properly when we eg. substitute function parameters for de Bruijn indices).

Then we can check to see if the contained environment for the actual proposition set satisfies the
supertype proposition.

Test case:

Notes

This test case should pass: let-filter-unscoping-test.

Code review:
Patch: