{motive : Lean.AxiomVal → Sort u} →
  ((toConstantVal : Lean.ConstantVal) →
      (isUnsafe : Bool) → motive { toConstantVal := toConstantVal, isUnsafe := isUnsafe }) →
    (t : Lean.AxiomVal) → motive t