Definition weqoncompl_ne_compute {X Y : UU} (w : X ≃ Y) (x : X) (neq_x : neqPred x) (neq_wx : neqPred (w x)) x' : pr1 (weqoncompl_ne w x neq_x neq_wx x') = w (pr1 x'). Proof. intros. apply idpath. Defined.