Merge of last trunk commits

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