Autoinduct documentation improvement

[NeuralCoder3]

Many files in the autoinduct folder already have good documentation. However, the general ReadMe misses an introduction like given in ltac1. A redirect to ltac1 for motivation and ideas already helps. Furthermore, the MetaCoq part could use a bit more guidance on what the files are good for and how they are structured/how they operate.

This pull request extends the documentation and attempts to improve the points mentioned above.