Applies simplification bottom-up to all subterms, retraversing changed ones.
DESCRIPTION
HOL Light's simplification functions (e.g. SIMP_TAC) have their traversal
algorithm controlled by a ``strategy''. REDEPTH_SQCONV is a strategy
corresponding to REDEPTH_CONV for ordinary conversions: simplification is
applied bottom-up to all subterms, retraversing changed ones.