| Do I have to hoist the forall quantifiers in bla -> forall a=20 | . blub myself? At least, the code typechecks then. Sigh. I forgot to make the forall-hoisting feature apply recursively when I added the rank-N stuff. It's a 2 line change to make it so, but it is a change. Workaround: do the forall-hoisting yourself. Sorry. Simon