On Wed, Feb 05, 2014 at 08:24:23AM +0100, Ulf Norell wrote: > I would make X and Y implicit. That's in line with the other cong functions > and as you say, they can often be inferred. I'm sorry, but that doesn't work. At the very least X must be explicit (like P is explicit for subst). The question was only about Y. Helmut