∀ {M : Type u_1} {α : Type u_4} [inst : Monoid M] {c : Con M} (u : c.Quotientˣ)
  (f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α)
  (Hf :
    ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
      c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'),
  Con.liftOnUnits u f Hf = Con.hrecOn₂ (↑u) (↑u⁻¹) (fun x y hxy hyx => f x y ⋯ ⋯) ⋯ ⋯ ⋯