? x ? should squash

[heades]

Currently, we only squash function types. That is, types of the form ? -> ?. However, this will prevent the proof we need from going through, because the Siek:13 language allows for types of the form ? x ? to be squashed. I think we need to add this to our system.