Lemma isaninv1 (X : UU) : isdecprop X -> isaninvprop X. Proof. intros is1. unfold isaninvprop. assert (is2 := pr1 is1); simpl in is2. assert (adjevinv: dneg X -> X). {intro X0. induction is2 as [ a | b ]. - assumption. - contradicts X0 b. } assert (is3: isaprop (dneg X)). {apply (isapropneg (X -> empty)). } apply (isweqimplimpl (todneg X) adjevinv is1 is3). Defined.