Remove uses of axioms

[Lysxia]

Closes #72

There is one inversion lemma left which necessitates UIP, which is eqit_Vis_inv. It's actually not as useful as it seems (the tutorial example doesn't use it), but when you do run into it, it's very hard to do without (one can try using eqit_Vis_inv_weak instead).

There may be some way of strengthening eqitF so that eqit_Vis_inv is provable. That's Future Work™.

• [x] Think about organizing lemma names
• [x] Document status of axioms in library (basically, we try to avoid axioms, but I think itrees may be especially counterintuitive to use without UIP, i.e., without eqit_Vis_inv)
• [x] Check compatibility with older versions of paco

---

JMeq_eq/UIP is the main axiom we use. It is used by pcofix/etc. and more directly in various places.

• [x] Override the pcofix, gcofix, and ecofix tactics to not use axioms (ideally this should be implemented in paco, but these new implementations have performance issues for relations of high arity, so we just provide them locally for now)
• [x] Don't use dependent destruct
• [x] Weaken inversion lemmas (there are still some places where we use Vis e k1 = Vis e k2 -> k1 = k2, which is actually not provable without JMeq_eq)

[Lysxia]

The tutorial is now CLOSED UNDER THE GLOBAL CONTEXT, i.e., it does not use any axiom anymore.

The library still contains lemmas that depend on axioms (most notably eqit_Vis_inv). I'll leave it there because doing some stuff without it seems hard (using eqit_Vis_inv_weak instead). The library itself makes no use of that particular lemma at the moment though.

There may be some way of strengthening eqitF so that eqit_Vis_inv is provable.