{motive : Lean.StructureResolutionOrderResult → Sort u} →
  ((resolutionOrder : Array Lean.Name) →
      (conflicts : Array Lean.StructureResolutionOrderConflict) →
        motive { resolutionOrder := resolutionOrder, conflicts := conflicts }) →
    (t : Lean.StructureResolutionOrderResult) → motive t