Okay, but why doesn't that just work? If I have something like:
```
syntax Int ::= foo(Int) [function]
rule foo(I:Int) => foo(I -Int 1) when I >Int 0
```

it should still work to try to match I -Int 1 against I:Int, because of how the matching process should treat variables. Right?