{α : Type u} →
  [inst : AddGroup α] →
    {motive : AddGroupTopology α → Sort u_1} →
      (t : AddGroupTopology α) →
        ((toTopologicalSpace : TopologicalSpace α) →
            (toIsTopologicalAddGroup : IsTopologicalAddGroup α) →
              motive { toTopologicalSpace := toTopologicalSpace, toIsTopologicalAddGroup := toIsTopologicalAddGroup }) →
          motive t