{motive : Lean.DefinitionSafety → Sort u} →
  (t : Lean.DefinitionSafety) →
    motive Lean.DefinitionSafety.unsafe →
      motive Lean.DefinitionSafety.safe → motive Lean.DefinitionSafety.partial → motive t