(motive : Lean.Meta.RefinedDiscrTree.Key → Sort u_1) →
  (x : Lean.Meta.RefinedDiscrTree.Key) →
    (Unit → motive Lean.Meta.RefinedDiscrTree.Key.star) →
      ((id : ℕ) → motive (Lean.Meta.RefinedDiscrTree.Key.labelledStar id)) →
        (Unit → motive Lean.Meta.RefinedDiscrTree.Key.opaque) →
          ((name : Lean.Name) → (nargs : ℕ) → motive (Lean.Meta.RefinedDiscrTree.Key.const name nargs)) →
            ((fvarId : Lean.FVarId) → (nargs : ℕ) → motive (Lean.Meta.RefinedDiscrTree.Key.fvar fvarId nargs)) →
              ((idx nargs : ℕ) → motive (Lean.Meta.RefinedDiscrTree.Key.bvar idx nargs)) →
                ((v : Lean.Literal) → motive (Lean.Meta.RefinedDiscrTree.Key.lit v)) →
                  (Unit → motive Lean.Meta.RefinedDiscrTree.Key.sort) →
                    (Unit → motive Lean.Meta.RefinedDiscrTree.Key.lam) →
                      (Unit → motive Lean.Meta.RefinedDiscrTree.Key.forall) →
                        ((name : Lean.Name) →
                            (idx nargs : ℕ) → motive (Lean.Meta.RefinedDiscrTree.Key.proj name idx nargs)) →
                          motive x