Continuing NoCycle: dependent types.
Continuing NoCycle: dependent types.

This is not so convincing:
- It seems hard to automatize.
- It does not seem very useful in that case (if you can write
  [v1 = v2], then a simple argument on the indexes of [v1] and
  [v2] should prove that one is not a subterm of the other).
- It relies on the decidability of the equality of the indexes.
- I could not make it work easily in the case of indexes which
  are not directly built by constructors: for instance, if you
  take the type of lists indexed by the parity of their length
  (same type, replacing [nat] by [bool] and [S] by [negb], then
  you need some argument of injectivity on [negb], and once
  again, this does not seem easy to do automatically.

mattam82/Coq-Equations,mattam82/Coq-Equations