proposition: Lemma eqfromdnegeq (X : UU) (is : isdeceq X) (x x' : X) : dneg (x = x') -> x = x'.
proof: Proof. intros X0. induction (is x x') as [ y | n ]. - assumption. - induction (X0 n). Defined.
imports: UniMath.Foundations.PartA