∀ {α : Type u_1} {β : Type u_2} [inst : AddGroup β] (f : α → β) (a b : FreeAddGroup α),
  Quot.lift (FreeAddGroup.Lift.aux f) ⋯ (a + b) =
    Quot.lift (FreeAddGroup.Lift.aux f) ⋯ a + Quot.lift (FreeAddGroup.Lift.aux f) ⋯ b