{α : Type} →
  {P : Sort u} →
    {tree : Lean.Meta.RefinedDiscrTree.PreDiscrTree α} →
      {errors : Array Lean.Meta.RefinedDiscrTree.ImportFailure✝} →
        {tree' : Lean.Meta.RefinedDiscrTree.PreDiscrTree α} →
          {errors' : Array Lean.Meta.RefinedDiscrTree.ImportFailure✝¹} →
            { tree := tree, errors := errors } = { tree := tree', errors := errors' } →
              (tree ≍ tree' → errors = errors' → P) → P