From Greg Price:

This week, we implemented rule generation and discrimination trees.  We have
finalized the datatypes for rules and sequents.