{motive : ProfiniteAddGrp.{u_1} → Sort u} →
  (t : ProfiniteAddGrp.{u_1}) →
    ((toProfinite : Profinite) →
        [addGroup : AddGroup ↑toProfinite.toTop] →
          [topologicalAddGroup : IsTopologicalAddGroup ↑toProfinite.toTop] →
            motive { toProfinite := toProfinite, addGroup := addGroup, topologicalAddGroup := topologicalAddGroup }) →
      motive t