Updated the focusing example to the HH version
Change the version number to 2.0.0
Also change the version number in 'Makefile' to 2.0.0
Deleted the strong normalization example from Alwen Tiu and the big lambda-sigma calculus example. Maybe we can update them to the HH version in the future.
Correct the name 'debrujin' to be 'debruijn'
Modified the proof for type uniqueness to be consistent with the new advanced walkthrough for Abella
Updated the type uniqueness example for the advanced walkthrough