Indexed Coinduction

[gilhur]

I implemented a much nicer coinduction + induction principle, which is (well-founded) indexed coinduction rather than mixed induction-coinduction.

It works beautifully eliminating the necessity of "eutt.v", only requiring "eq.v". It completely removes all the ugly parts of our CPP paper (ie, the weird relation with four assumptions). I only updated 90% of eq.v and the rest of ITrees development is untouched.

I presented the ideas to Steve, Yannick, and Paul, who can review this pr.

[YaZko]

Thanks for the presentation and the PR Gil, that's looking great! I'll work my way through it in the incoming days.

[gilhur]

Thanks Yannick. Let's discuss further once you review the code.

[Lysxia]

oops