∀ {α : Type u_1} (motive : FreeAddMagma α → Sort u_2) (x : α) (h_1 : (x : α) → motive (FreeAddMagma.of x))
  (h_2 : (x y : FreeAddMagma α) → motive (x.add y)),
  (match FreeAddMagma.of x with
    | FreeAddMagma.of x => h_1 x
    | x.add y => h_2 x y) =
    h_1 x