This repository contains a proof of pi injectivity for an untyped equational theory with surjective pairing and extensionality.