Definition weqneghexistsnegtotal2 {X : UU} (P : X -> UU) : weq (neg (hexists P)) (neg (total2 P)). Proof. intros. assert (lg : (neg (hexists P)) <-> (neg (total2 P))). { split. - apply (negf (total2tohexists P)). - intro nt2. unfold neg. change (ishinh_UU (total2 P) -> hfalse). apply (hinhuniv). apply nt2. } apply (weqimplimpl (pr1 lg) (pr2 lg) (isapropneg _) (isapropneg _)). Defined.