{R : Ring} {I : Ideal R} (P : R / I -> Type) `{forall x, IsHSet (P x)} (c : forall (x : R), P (rng_quotient_map I x)) (g : forall (x y : R) (h : I (- x + y)), qglue h # c x = c y) : forall (r : R / I), P r := Quotient_ind _ P c g.
Require Import WildCat.Core WildCat.Equiv. Require Import Algebra.Congruence. Require Import Algebra.AbGroups. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Rings.Ring. Require Import Algebra.Rings.Ideal. Import Ideal.Notation.