Empty natural transformation in yellow-safe constraint

[shingarov]

The following should typecheck trivially (yellow safe), as there are no refinements. Instead, it crashes due to empty natural transformation:

⟦measure len : list(''a) => int⟧
type list(''a) =
  | Nil                        => [v| v∘len === 0]
  | Cons (x:''a, xs:list(''a)) => [v| v∘len === (xs∘len + 1)]
  ;
⟦val range : i:int => j:int => list(int) ⟧
let rec range = (i, j) => {
  let cond = i < j;
  if (cond) {
    let i1 = i + 1;
    let tl = range(i1, j);
    Cons(i, tl)
  } else {
    Nil
  }
};

This stands in the way of L₇ test range. We delay this problem until we have datatypes over Z3 datatypes.