MM Tool: Metamath editor
Load:
Prefix
Verify
Verify All
Main code
Output