{motive : Lean.Meta.Grind.EMatchTheoremKind → Sort u} →
  (t : Lean.Meta.Grind.EMatchTheoremKind) →
    t.ctorIdx = 1 → ((gen : Bool) → motive (Lean.Meta.Grind.EMatchTheoremKind.eqRhs gen)) → motive t