We extend classical first-order logic with subtyping by type
predicates and type coercion. Type predicates assert that the value of
a term belongs to a more special type than the signature guarantees,
while type coercion allows using terms of a more general type where the
signature calls for a more special one. These operations are important
e.g. in the specification and verification of object-oriented programs. We
present a tableau calculus for this logic and prove its completeness.