Wingman: Destruct on let-bound term fails

[isovector]

data IntroParams
  = IntroduceAllUnnamed
  | IntroduceOnlyNamed [OccName]
  | IntroduceOnlyUnnamed Int
  deriving stock (Eq, Ord, Show)

intros'
    :: IntroParams
    -> TacticsM ()
intros' params = rule $ \jdg -> do
  let g  = jGoal jdg
  case tacticsSplitFunTy $ unCType g of
    (_, _, [], _) -> cut -- failure $ GoalMismatch "intros" g
    (_, _, args, res) -> do
      ctx <- ask
      let occs = _

trying Desruct params at the hole produces:

      let occs = _
          occs = _
          occs = _

Yikes.

[isovector]

But this feels very similar to something I fixed in #2049, so maybe it's fixed and I'm just running an old version.

[isovector]

This is is not fixed in master. I'll investigate.

[isovector]

My test might have been invalidated by #2076. Either way, I'll write a test for this and get it checked in to use the power of CI.

[isovector]

This is working in HEAD.