Complete conversion properties theory.

As expected/hoped, the functions that convert from concrete syntax
trees into abstract syntax trees are total on all well-formed (wrt the
CFG) parse-trees.