∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {A B : Finset G} {a0 b0 : G} [inst_2 : DecidableEq H]
  (f : G →ₙ+ H),
  Function.Injective ⇑f → (UniqueAdd (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0) ↔ UniqueAdd A B a0 b0)