Definition weqoncompl_ne {X Y : UU} (w : X ≃ Y) (x : X) (neq_x : neqPred x) (neq_wx : neqPred (w x)) : compl_ne X x neq_x ≃ compl_ne Y (w x) neq_wx. Proof. intros. intermediate_weq (∑ x', neq_wx (w x')). - apply weqfibtototal; intro x'. apply weqiff. {apply (logeq_trans (Y := x != x')). {apply issymm_logeq, negProp_to_iff. } apply (logeq_trans (Y := w x != w x')). {apply logeqnegs. apply weq_to_iff. apply weqonpaths. } apply negProp_to_iff. } {apply negProp_to_isaprop. } {apply negProp_to_isaprop. } - refine (weqfp _ _). Defined.