[grasshopper] Let procedures / post-condition refer to pre-condition footprint

[septract]

Right now we existentially quantify the footprint separately for the pre/post. We might want to rearrange this so we quantify the pre-footprint in the procedure argument, because this would mean we could compare the pre/post footprint, and refer to it explicitly in procedure calls.

[MattWindsor91]

Would this at all help with problems relating to assignment? Eg. being able to pure-assume that e is not in the pre-condition footprint. Or is the problem here entirely due to the postcondition?