(P : (forall i, A i / R i) -> Type) `{!forall g, IsHProp (P g)} (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i))) (g : forall i, A i / R i) : P g. Proof. refine (choose_quotient_ind P a _ g). intros. apply path_ishprop. Defined.
Require Import