∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, P f → Q f) →
    ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
      RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f →
        RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => Q) f