{R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          Function.Bijective ⇑(algebraMap R S) → Algebra.Presentation R S PEmpty.{w + 1} PEmpty.{t + 1}