Improve documentation on some topics

[filipeom]

Some very interesting feedback we got from Martin. Documentation and examples might help a ton here. Also, maybe some better APIs? Will see

# Typing and symbols

## Typing of relop

If I've correctly understood, expressions have to be annotated with types when
using the constructor functions `Expr.binop`, `Expr.relop` etc. It is however
not clear to me what the type of a relop refers to: the type of the resulting
expression, or of its arguments. The former seems more coherent because it
would easily generalize to n-ary function application with arguments of
different types (however also see below), but the Smtml implementation seems to behave
differently. When representing the term `x < 1` by

```
let ex_one =
    let x = Expr.symbol (Symbol.make Ty.Ty_int "x") in
    let one = Expr.value (Value.Int 1) in
    Expr.(relop Ty_bool Ty.Relop.Lt x one)
```

I get a `Fatal error: exception Failure("Bool: Unsupported Z3 relop operator \"lt_s\"")`
(NB: I'm working with Alt-Ergo), whereas `Expr.(relop Ty_int Ty.Relop.Lt x one)`
behaves correctly.

## Declaration of symbols

In module `Symbol`, there are several functions for symbol creation.

* Is the operator `(@:)` the same as `make`, with arguments swapped?
* Are these two just instances of `make3` with namespace `Term`?
* I guess `mk` is for creating sorts (see below)?

I assume that `make` is mapped to a `declare-const` in SMT-LIB. How are
several subsequent calls to `make` with the same name handled? Are they cached
to have the effect of a single `declare-const` only, or does the client of Smtml have to take care of declaring a single instance for each symbol?

# Correspondence between Smtml and SMT-Lib
## Sorts

I assume that a 0-ary sort `s` can be defined by `Symbol.mk Symbol.sort s`,
corresponding to an SMT-LIB declaration `(declare-sort s 0)`.
What about sorts of higher arity?

## Functions
How to declare uninterpreted function symbols, something corresponding for
example to `(declare-fun f (Int Bool) Int)` in SMT-LIB?

## Function application

How would one write a function application, something like `(f 1 true)`? In
this context, what is the "application type" `Ty_app`?