{motive : Lean.Meta.Grind.EMatchTheoremKind → Sort u} →
  (t : Lean.Meta.Grind.EMatchTheoremKind) →
    ((gen : Bool) → motive (Lean.Meta.Grind.EMatchTheoremKind.eqBoth gen)) →
      (Nat.hasNotBit 4 t.ctorIdx → motive t) → motive t