∀ {F : Type u_9} {A : outParam (Type u_10)} {B : outParam (Type u_11)} {inst : Add A} {inst_1 : Add B}
  {inst_2 : EquivLike F A B} [self : AddEquivClass F A B] (f : F) (a b : A), f (a + b) = f a + f b