{P : Sort u_1} →
  {α : Type u} →
    {inst : AddMonoid α} →
      {t : AddUnits α} →
        {α' : Type u} →
          {inst' : AddMonoid α'} → {t' : AddUnits α'} → α = α' → inst ≍ inst' → t ≍ t' → AddUnits.noConfusionType P t t'