(motive : Lean.Meta.Grind.EMatchTheoremKind → Sort u_1) →
  (x : Lean.Meta.Grind.EMatchTheoremKind) →
    ((gen : Bool) → motive (Lean.Meta.Grind.EMatchTheoremKind.eqLhs gen)) →
      ((gen : Bool) → motive (Lean.Meta.Grind.EMatchTheoremKind.eqRhs gen)) →
        ((gen : Bool) → motive (Lean.Meta.Grind.EMatchTheoremKind.eqBoth gen)) →
          (Unit → motive Lean.Meta.Grind.EMatchTheoremKind.eqBwd) →
            (Unit → motive Lean.Meta.Grind.EMatchTheoremKind.fwd) →
              ((gen : Bool) → motive (Lean.Meta.Grind.EMatchTheoremKind.bwd gen)) →
                (Unit → motive Lean.Meta.Grind.EMatchTheoremKind.leftRight) →
                  (Unit → motive Lean.Meta.Grind.EMatchTheoremKind.rightLeft) →
                    ((gen : Bool) → motive (Lean.Meta.Grind.EMatchTheoremKind.default gen)) →
                      (Unit → motive Lean.Meta.Grind.EMatchTheoremKind.user) → motive x