Formalize approximation of terms not reducing to 0

[jgbm]

Suppose that the predicate P represents the property we care about. Then we need two properties: $P\ t \to \neg (t \leadsto 0)$ and $P\ t \to t \leadsto t' \to P\ t'$. Most likely, this property will need to be a logical relation (i.e., with respect to the type classifying the term). Some existing work has shown that ContainsVariant [.guard, .term, .var .openm, .var .term] t is a valid P, but it's too restrictive. It's useful to view P as a normalization property for a subset of $F_D$ syntax.