Coq proofs related to the VSTTE'15 paper titled "Machine-checked proofs for realizability checking algorithms".