{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} →
  {motive : RingHom.PropertyIsLocal P → Sort u_1} →
    ((localizationAwayPreserves : RingHom.LocalizationAwayPreserves P) →
        (ofLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget P) →
          (ofLocalizationSpan : RingHom.OfLocalizationSpan P) →
            (StableUnderCompositionWithLocalizationAwayTarget :
                RingHom.StableUnderCompositionWithLocalizationAwayTarget P) →
              motive ⋯) →
      (t : RingHom.PropertyIsLocal P) → motive t