∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M → N) (H : ∀ (x y : M), f (x * y) = f x * f y)
  (c : Con N), Con.comap f H c = { toSetoid := Setoid.comap f c.toSetoid, mul' := ⋯ }