If conv N returns A |- N = P, then BINDER_CONV conv (M (\v.N)) returns
A |- M (\v.N) = M (\v.P) and BINDER_CONV conv (\v.N) returns
A |- (\v.N) = (\v.P)
FAILURE
If conv N fails, or if v is free in A.
EXAMPLE
- BINDER_CONV SYM_CONV (Term `\x. x + 0 = x`);
> val it = |- (\x. x + 0 = x) = \x. x = x + 0 : thm
COMMENTS
For deeply nested quantifiers, STRIP_BINDER_CONV and
STRIP_QUANT_CONV are more efficient than iterated application of
BINDER_CONV, BINDER_CONV, or ABS_CONV.