Start specialising Expr
Finish reworking Expr
Keep Coq code up to date