proposition: Lemma isaprop_istotal {X : hSet} (R : hrel X) : isaprop (istotal R).
proof: Proof. intros. unfold istotal. apply impred; intro x. apply impred; intro y. apply propproperty. Defined.
imports: UniMath.Foundations.Propositions