Sound and complete subtyping between coinductive types for object-oriented languages