∀ {α : Type u} [inst : DecidableEq α] {a b : α × Bool} (L : List (α × Bool)),
  FreeAddGroup.reduceCyclically (a :: (L ++ [b])) =
    if b.1 = a.1 ∧ (!b.2) = a.2 then FreeAddGroup.reduceCyclically L else a :: L ++ [b]