proposition: Lemma isdecnegrel {X : UU} (R : hrel X) (isr : isdecrel R) : isdecrel (negrel R).
proof: Proof. intros. intros x1 x2. induction (isr x1 x2) as [ r | nr ]. - apply ii2. apply (todneg _ r). - apply (ii1 nr). Defined.
imports: UniMath.Foundations.Propositions