This repository hosts a proof written in the Gallina language. We use the Coq automated theorem prover to prove the equivalence of two semantics defined over a toy process algebra.
A web page (generated with coqdoc) presenting the proof can be accessed here.