{P : Sort u} →
  {M : Type u_12} →
    {A : Type u_13} →
      {inst : Zero A} →
        {t : SMulZeroClass M A} →
          {M' : Type u_12} →
            {A' : Type u_13} →
              {inst' : Zero A'} →
                {t' : SMulZeroClass M' A'} →
                  M = M' → A = A' → inst ≍ inst' → t ≍ t' → SMulZeroClass.noConfusionType P t t'