{P : Sort u} →
  {cur : Lean.Syntax} →
    {parents : Array Lean.Syntax} →
      {idxs : Array ℕ} →
        {cur' : Lean.Syntax} →
          {parents' : Array Lean.Syntax} →
            {idxs' : Array ℕ} →
              { cur := cur, parents := parents, idxs := idxs } = { cur := cur', parents := parents', idxs := idxs' } →
                (cur = cur' → parents = parents' → idxs = idxs' → P) → P