∀ {α : Type u} [inst : DecidableEq α] (L : List (α × Bool)),
  FreeAddGroup.reduceCyclically.conjugator L ++ FreeAddGroup.reduceCyclically L ++
      FreeAddGroup.negRev (FreeAddGroup.reduceCyclically.conjugator L) =
    L