∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.IsReduced L →
    ∀ (n : ℕ),
      FreeAddGroup.reduce (List.replicate (n + 1) L).flatten =
        FreeAddGroup.reduceCyclically.conjugator L ++
            (List.replicate (n + 1) (FreeAddGroup.reduceCyclically L)).flatten ++
          FreeAddGroup.negRev (FreeAddGroup.reduceCyclically.conjugator L)