(motive : Lean.Meta.DiscrTree.Key × Array Lean.Expr → Sort u_1) →
  (x : Lean.Meta.DiscrTree.Key × Array Lean.Expr) →
    ((k : Lean.Meta.DiscrTree.Key) → (todo : Array Lean.Expr) → motive (k, todo)) → motive x