Description: An inference for distributing quantifiers over a nested implication.
The canonical derivation from its closed form bj-exalim (using mpg )
has fewer essential steps, but more steps in total (yielding a longer
compressed proof). (Almost) the general statement that speimfw proves. (Contributed by BJ, 29-Sep-2019)