@kha I added this example as a template for what the equation compiler
will have to do. The plan is:
- We can use `partial` to define any function if the result type is
inhabited.
- If the result type is of the form `Partial a`, the equation compiler
generates lemmas of the form:
```
theorem fooEq args : terminates (foo args) → foo args = lhs
```
The new test contains an example.
