{R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        {inst : CommRing R} →
          {inst_1 : CommRing S} →
            {inst_2 : Algebra R S} →
              {P : Sort u_1} →
                {toGenerators : Algebra.Generators R S ι} →
                  {relation : σ → toGenerators.Ring} →
                    {span_range_relation_eq_ker : Ideal.span (Set.range relation) = toGenerators.ker} →
                      {toGenerators' : Algebra.Generators R S ι} →
                        {relation' : σ → toGenerators'.Ring} →
                          {span_range_relation_eq_ker' : Ideal.span (Set.range relation') = toGenerators'.ker} →
                            { toGenerators := toGenerators, relation := relation,
                                  span_range_relation_eq_ker := span_range_relation_eq_ker } =
                                { toGenerators := toGenerators', relation := relation',
                                  span_range_relation_eq_ker := span_range_relation_eq_ker' } →
                              (toGenerators ≍ toGenerators' → relation ≍ relation' → P) → P