• Reworking the Standard Library
• Finite Types
• Extensional Equality
• Wf
• Theory of relations
• Order stuff (8.3)
• Consistent Definition of Operators
• Is_true vs (true=)
• Arithmetic
• Set theory
• Abstract algebra
• Double-negation mapping of classical logic
• Interfaces and Types
• Structure
• Organization