{α : Type u} →
  {P : Sort u_1} →
    {toCommSemiring : CommSemiring α} →
      {toSemilatticeSup : SemilatticeSup α} →
        {add_eq_sup : autoParam (∀ (a b : α), a + b = a ⊔ b) IdemSemiring.add_eq_sup._autoParam} →
          {bot : α} →
            {bot_le : ∀ (a : α), bot ≤ a} →
              {toCommSemiring' : CommSemiring α} →
                {toSemilatticeSup' : SemilatticeSup α} →
                  {add_eq_sup' : autoParam (∀ (a b : α), a + b = a ⊔ b) IdemSemiring.add_eq_sup._autoParam} →
                    {bot' : α} →
                      {bot_le' : ∀ (a : α), bot' ≤ a} →
                        { toCommSemiring := toCommSemiring, toSemilatticeSup := toSemilatticeSup,
                              add_eq_sup := add_eq_sup, bot := bot, bot_le := bot_le } =
                            { toCommSemiring := toCommSemiring', toSemilatticeSup := toSemilatticeSup',
                              add_eq_sup := add_eq_sup', bot := bot', bot_le := bot_le' } →
                          (toCommSemiring ≍ toCommSemiring' → toSemilatticeSup ≍ toSemilatticeSup' → bot ≍ bot' → P) → P