Coinductive subtyping for abstract compilation of object-orientedlanguages into Horn formulas