{u v : Lean.Level} →
  {motive : Qq.MaybeLevelDefEq u v → Sort u} →
    (t : Qq.MaybeLevelDefEq u v) →
      ((a : u =QL v) → motive (Qq.MaybeLevelDefEq.defEq a)) → motive Qq.MaybeLevelDefEq.notDefEq → motive t