Reynolds's abstraction theorem, often referred to as the parametricity theorem, can be used to derive properties about functional programs solely from their types. Unfortunately, in the presence of runtime type analysis, the abstraction properties of polymorphic programs are no longer valid. However, runtime type analysis can be implemented with term-level representations of types, as in the lambda_R language of Crary et al., where case analysis on these runtime representations introduces type refinement. In this paper, we show that representation-based analysis is consistent with type abstraction by extending the abstraction theorem to such a language. We also discuss the "free theorems" that result. This work provides a foundation for the more general problem of extending the abstraction theorem to languages with generalized algebraic datatypes (GADTs).