feat(logic/basic): Add forall_apply_eq_imp_iff (#4109)
Also adds forall_apply_eq_imp_iff' for swapped forall arguments
This means that `forall_range_iff` can now be solved by `simp`.
This requires changes in data/pfun and measure_theory/borel_space, where non-terminal `simp`s broke.
