Outil conçu pour simplifier des preuves formelles écrites en Lean en éliminant certaines égalités définitionnelles. Il facilite la traduction de ces preuves vers d'autres systèmes comme Coq tout en permettant une forme limitée d'extensionalité simulée dans Lean. Le projet s'appuie sur des traductions extensionales vers intensionales pour rendre les preuves plus portables et vérifiables.