Zippers for terms. More option-based functions.
Abduction for terms: initial commit of completed algorithm.
Complex list operations (concat_fold, product).
to_formula translates substitution to atoms.