We consider a version of the Mitchell's polymorphic type containment (aka subsumption). Here, it is not suited for the system F but for the predicative version of it introduced by Leivant. The aim of the approach is to propose a new notion of polymorphic functional subsumption
which may be decidable unlike Mitchell's one. We define a system for predicative subsumption in the style of Mitchell and
then prove its equivalence with a Gentzen-style definition. Next, we study the notion of bicoercibility. This is followed
by a reduction of the typability in the Leivant's system with subsumption to subsumption itself.