∀ (Q Q_1 : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop),
  Q = Q_1 →
    ∀ ⦃X Y : AlgebraicGeometry.Scheme⦄ (x x_1 : X ⟶ Y),
      x = x_1 →
        ∀ [inst : AlgebraicGeometry.IsAffine Y], AlgebraicGeometry.affineAnd Q x = AlgebraicGeometry.affineAnd Q_1 x_1