Clean FOLowerUnits
Change theorem proof

Added induction; some notation changes (more to come).