In this paper, we present a general strategy that enables the translation of tableau proofs using different Skolemization rules into machine-checkable proofs. It is part of a framework that enables (i) instantiation of the strategy into algorithms for different set of tableau rules (e.g., different logics) and (ii) easy soundness proof which relies on the local extensibility of user-defined rules. Furthermore, we propose an instantiation of this strategy for first-order tableaux that handles notably δ++ rules, which is, as far as the authors know, the first one in the literature. Additionally, this deskolemization strategy has been implemented in the Goéland automated theorem prover, enabling an export of its proofs in Coq and Lambdapi. Finally, we have evaluated the algorithm performances for δ+ and δ++ rules through the certification of proofs from some categories of the TPTP library.