Bring written rules up to date with Redex model.

- loose expansion
- no more wfe