{motive_1 : Lean.Elab.Term.Do.Code → Sort u} →
  (t : Lean.Elab.Term.Do.Code) →
    t.ctorIdx = 9 →
      ((ref gen discrs optMotive : Lean.Syntax) →
          (alts : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
            motive_1 (Lean.Elab.Term.Do.Code.match ref gen discrs optMotive alts)) →
        motive_1 t