Preconditions on arguments don't satisfy subsequent calls with the same precondition

```
pred p(int i) -> bool { true }

fn f(int i) : p(i) -> int { i }

fn g(int i) : p(i) -> int { f(i) }
```

Function g doesn't typecheck because the precondition on f isn't satisfied. I would expect this to work, otherwise I can't push the responsibility for satisfying preconditions up the call stack.
