{F : Type u_9} →
  {A : Type u_10} →
    {B : Type u_11} →
      [inst : Mul A] →
        [inst_1 : Mul B] →
          [inst_2 : EquivLike F A B] →
            {motive : MulEquivClass F A B → Sort u} →
              (t : MulEquivClass F A B) → ((map_mul : ∀ (f : F) (a b : A), f (a * b) = f a * f b) → motive ⋯) → motive t