Fix a bug with comprehension checking

  Wasn't relating the size of the goal type to the size of the arms of the
comprehension.
Avoid redundant cases
Remove unused inferFun function