added two more files/chapters, added example 2.1 both ast and coq version, added description