mlSimpl should be renamed to mlPropagateSubst, because it only propagates substitutions currently into the subpatterns. On top of this tactic, we can define mlSimpl which actually simplifies the propagated substitutions (which also includes removing bound variable substitution for closed pattern).
mlSimplshould be renamed tomlPropagateSubst, because it only propagates substitutions currently into the subpatterns. On top of this tactic, we can definemlSimplwhich actually simplifies the propagated substitutions (which also includes removing bound variable substitution for closed pattern).