Definition iscontrsecoverempty2 {X : UU} (P : X -> UU) (is : neg X) : iscontr (∏ x, P x). Proof. intros. set (w := weqtoempty is). set (w' := weqonsecbase P (invweq w)). apply (iscontrweqb w' (iscontrsecoverempty _)). Defined.