linter.fugue.simpIntro

When a subgoal is intro'd only to be finished by a bare closing simp, simp_intro does both — it introduces the binders and simplifies as each arrives.