Add 'unit'
Add pairs and prove progress theorem for them
Extend appears_free_in constructors and 'prove' the rest of the theorems for pairs