Tutorial Equations: index inductive types (#75)

* add draft tuto equations indexed ind

* fix file

* fix bugs

* add text on NoConfusion

* add text uip and inacessible patterns

* first draf

* Update Tutorial_Equations_indexed.v

* Typos, rephrasings and more explanations

* Apply suggestions for @thomas-lamiaux 's review

* Simpler introduction to [dependent elimination .. as .]

* Update gitignore

* Add to index.html

---------

Co-authored-by: thomas-lamiaux <[email protected]>
Co-authored-by: Thomas Lamiaux <[email protected]>

.gitignore

@@ -18,7 +18,6 @@
 *.vrb
 *.bcf
 *.run.xml
-*.html
 *.css
 *~
 node_modules/