This work investigates proof-theoretic methods for handling Henkin quantifiers within first-order logic. While such quantifiers extend expressiveness beyond standard first-order logic and are naturally representable in second-order logic, their direct treatment poses challenges for analytic proof systems and unification-based reasoning. Building on sequent calculi that incorporate Henkin quantifiers while preserving desirable properties such as cut-elimination and completeness relative to corresponding second-order systems, we introduce tableau systems with unification, enabling effective proof search while maintaining soundness and completeness.