{P sP} dclass dequiv x : @quotient_ind P sP dclass dequiv (class_of x) = dclass x. Proof. reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.