proposition: Lemma isapropaninvprop (X : UU) : isaninvprop X -> isaprop X.
proof: Proof. intros X0. apply (isofhlevelweqb (S O) (make_weq (todneg X) X0) (isapropdneg X)). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom