Implement ITrees manually

[Kiiyya]

Ideally we'd want to do the following:

codata ITree (E : Type -> Type) (A : Type) : Type 1
| ret : A -> ITree E A
| tau : ITree E A -> ITree E A
| vis {Ans : Type} : E Ans -> (Ans -> ITree E A) -> ITree E A

But due to some limitations we can't do that (yet), concretely because of the {Ans : Type} -> ... Pi binder. Hence this current implementation, which works around this issue by using a (Ans : Type) \x ... binder instead. This still leads to more issues:

• The qpf macro is not able to handle sigma types, see issue Make qpf macro support sigma types #50 .
• A lot of instances don't seem to get inferred properly. I have added a bunch of #synth and instance ... := inferInstance to help debug this.
• We want to have A : Type, but because all live type params have to live in the same universe, we must choose A : Type 1 and use ULifts. Unfortunately this is user-visible, since Shape and Base are user-visible when doing e.g. Cofix.corec or Cofix.dest