Predicativity in Rocq Equality in Mechanized Mathematics An inquiry into the Foundations of Mathematics ZFC and propositional logic Lean versus Rocq: The cultural chasm