  We introduce a sound and complete coinductive proof system for reachability
properties in transition systems generated by logically constrained term
rewriting rules over an order-sorted signature modulo builtins. A key feature
of the calculus is a circularity proof rule, which allows to obtain finite
representations of the infinite coinductive proofs.
