IxFree is a Coq library for shallow embedding of internal logic of step-indexed logical relations.

IxFree is tested to work with Coq version 9.1.0 and does not depend on any third-party library. It is recommended to build IxFree using dune build system (tested with version 3.20.2) and install it by opam.

Simply type dune build to compile the project. Then it can be installed by typing dune install.