∀ {α₁ : Type u_2} {α₂ : Type u_3} {α₃ : Type u_4} {rels₁ : FreeAddMonoid α₁ → FreeAddMonoid α₁ → Prop}
  {rels₂ : FreeAddMonoid α₂ → FreeAddMonoid α₂ → Prop} {rels₃ : FreeAddMonoid α₃ → FreeAddMonoid α₃ → Prop}
  {δ : PresentedAddMonoid rels₁ → PresentedAddMonoid rels₂ → PresentedAddMonoid rels₃ → Prop}
  (q₁ : PresentedAddMonoid rels₁) (q₂ : PresentedAddMonoid rels₂) (q₃ : PresentedAddMonoid rels₃),
  (∀ (a : FreeAddMonoid α₁) (b : FreeAddMonoid α₂) (c : FreeAddMonoid α₃),
      δ ((PresentedAddMonoid.mk rels₁) a) ((PresentedAddMonoid.mk rels₂) b) ((PresentedAddMonoid.mk rels₃) c)) →
    δ q₁ q₂ q₃