Blocking binders are now handled as part of the "regular"
meta-substitution. 
Added the factorial example.