proposition: Lemma isaprop_isantisymm {X : hSet} (R : hrel X) : isaprop (isantisymm R).
proof: Proof. intros. unfold isantisymm. apply impred; intro x. apply impred; intro y. apply impred; intro r. apply impred; intro s. apply setproperty. Defined.
imports: UniMath.Foundations.Propositions