An application subst_assoc P [{redex_1,residue_1},...,{redex_n,residue_n}]
returns SOME residue_i if P holds of redex_i, and did not hold
(or fail) for {redex_j | 1 <= j < i}. If P holds for none of
the redexes in the substitution, NONE is returned.
FAILURE
If P redex_i fails for some redex encountered in the left-to-right
traversal of the substitution.
EXAMPLE
- subst_assoc is_abs [T |-> F, Term `\x.x` |-> Term `combin$I`];
> val it = SOME`I` : term option