add heterogeneous substitutions, various cleanup

add notation, renaming predicates, and various facts about reduction

initial release