{R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] →
          {motive : Coalgebra R A → Sort u_1} →
            ([toCoalgebraStruct : CoalgebraStruct R A] →
                (coassoc :
                    ↑(TensorProduct.assoc R A A A) ∘ₗ
                        LinearMap.rTensor A CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul =
                      LinearMap.lTensor A CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul) →
                  (rTensor_counit_comp_comul :
                      LinearMap.rTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul =
                        (TensorProduct.mk R R A) 1) →
                    (lTensor_counit_comp_comul :
                        LinearMap.lTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul =
                          (TensorProduct.mk R A R).flip 1) →
                      motive
                        { toCoalgebraStruct := toCoalgebraStruct, coassoc := coassoc,
                          rTensor_counit_comp_comul := rTensor_counit_comp_comul,
                          lTensor_counit_comp_comul := lTensor_counit_comp_comul }) →
              (t : Coalgebra R A) → motive t