proposition: Lemma isdecreltoisnegrel {X : UU} {R : hrel X} (is : isdecrel R) : isnegrel R.
proof: Proof. intros. intros x1 x2. induction (is x1 x2) as [ r | nr ]. - intro. apply r. - intro nnr. induction (nnr nr). Defined.
imports: UniMath.Foundations.Propositions