{t : Type u → Type u → Type u} →
  {motive : Bitraversable t → Sort u_1} →
    (t_1 : Bitraversable t) →
      ([toBifunctor : Bifunctor t] →
          (bitraverse :
              {m : Type u → Type u} →
                [Applicative m] → {α α' β β' : Type u} → (α → m α') → (β → m β') → t α β → m (t α' β')) →
            motive { toBifunctor := toBifunctor, bitraverse := bitraverse }) →
        motive t_1