Added fbyn(expr, n, init) to encode init -> pre (init -> pre (init -> ... pre expr)) with n occurences of init