Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas