{u : Lean.Level} →
  {α :
      let u := u;
      Q(Sort u)} →
    {a b : Q(«$α»)} →
      {motive : Qq.MaybeDefEq a b → Sort u} →
        (t : Qq.MaybeDefEq a b) →
          ((a_1 : «$a» =Q «$b») → motive (Qq.MaybeDefEq.defEq a_1)) → motive Qq.MaybeDefEq.notDefEq → motive t