redex: unfold nts once during unification

Also:
* add a backtracking limit
* check for ground terms in both term and pat environments
  when filling in generated patterns
* update tests to be consistent with the above