Proving Soundness of Extensional Normal-Form Bisimilarities

Coq sources

Formalization was tested with Coq 8.6.