proposition: Lemma isapropiseqclass {X : UU} (R : hrel X) (A : hsubtype X) : isaprop (iseqclass R A).
proof: Proof. apply isofhleveldirprod. - exact (isapropishinh (carrier A)). - apply isofhleveldirprod. + repeat (apply impred; intro). exact (pr2 (A t0)). + repeat (apply impred; intro). exact (pr2 (R t t0)). Defined.
imports: UniMath.Foundations.Propositions