∀ {G : Type u_1} {H : Type u_3} {K : Type u_2} [inst : Add G] [inst_1 : Add H] [inst_2 : Add K] {a : G} {b : H} {c : K}
  (e₁ : AddConstEquiv G H a b) (e₂ : AddConstEquiv H K b c),
  Function.Semiconj (⇑e₂ ∘ ⇑e₁) (fun x => x + a) fun x => x + c