{R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        {motive : HopfAlgebraStruct R A → Sort u_1} →
          (t : HopfAlgebraStruct R A) →
            ([toBialgebra : Bialgebra R A] →
                (antipode : A →ₗ[R] A) → motive { toBialgebra := toBialgebra, antipode := antipode }) →
              motive t