We characterise type structurally the termination observational congruence of Abadi and Cardellipsilas Sforallcalculus. Pittspsila operational reasoning approach for polymorphic lambda calculi is enhanced with subtyping and primitive covariant object types. Labelling each object with a bound ordinal of terminating method invocations and regarding omega-bounded as unlabelled reduction we achieve a crucial object unwinding lemma. Value and term bisimilarities are suitably defined with novel type structural operators and (type-, relation- and value-environment) bindings. We prove term bisimilarity complete and sound with respect to observational congruence, postulated as the largest, substitutive, compatible, (termination) adequate and (type) subsumptive, well typed term relation.