fix(proof-libs/fstar): make t_Index.Output universe zero

[W95Psp]

Output is an associated type, and wasn't constrainted in terms of universes. Thus, F* would fail unifying types while using this instance because the associated type could be of any universe. This is causing the failure in cryspen/libcrux#177.

[karthikbhargavan]

Ah yes, I did not see this. I approve, but can you do a search through all the libraries to fix all universes to 0? E.g. I think. we used 'a in some places, and I removed those, but am not sure I got everything.

[W95Psp]

I think things are fine, the library is type-checking just fine! Will look for 'a anyway just in case
Though, I've just pushed a commit that propagates this Type0 for every occurrence of "associated type"/type families in typeclasses.

EDIT: ah, now I have regressions