Modifications to translation:
Be very careful to not inline since I want to use
projections instead of quantified variables in pattern matches
Re-introducing min in guards and removing minrec for
now, in order to get the model printing out to work.