Incomplete chapters

Some topics yet to be written:

• Elaborate on the proof procedure
• SLG solving – introduce negative reasoning
• Go over how trait impls are selected and checked
• Add a section on higher-ranked trait bounds