(n : Q(ℕ)) →
  (motive : Qq.MaybeDefEq n q(0) → Sort u_1) →
    (__do_lift : Qq.MaybeDefEq n q(0)) →
      ((pf : «$n» =Q 0) → motive (Qq.MaybeDefEq.defEq pf)) → (Unit → motive Qq.MaybeDefEq.notDefEq) → motive __do_lift