{motive : Lean.Meta.NativeEqTrueResult → Sort u} →
  ((prf : Lean.Expr) → motive (Lean.Meta.NativeEqTrueResult.success prf)) →
    motive Lean.Meta.NativeEqTrueResult.notTrue → (t : Lean.Meta.NativeEqTrueResult) → motive t