Thanks to Pino Rosolini for pointing out a typo in my formula: for any function f:Sigma x X -> Sigma (not -> X) and predicate a:X -> Sigma f(a) & a = f(true) & a where the parameter x has been suppressed from the equation so in full it reads, less clearly f(a(x),x) & a(x) = f(true,x) & a(x) Paul