forall P sP dclass dequiv, forall x y (H : R x y), apD (@quotient_ind P sP dclass dequiv) (related_classes_eq H) = dequiv x y H.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.