Added existentially quantified properties
Refactoring

  Better names
  Sections