Each node corresponds to a theorem statement. The different colors represent the 17 different modules. Higher color opacities represent nodes with more dependencies, and lower color opacities represent those with fewer. Clicking on any node will show its direct dependencies and dependents, not including the recursive enumeration of dependencies and dependents.
-- Rocq source code will appear here --
-- Lean translation will appear here --
-- Rocq ISO proof will appear here --