Change FOLowerUnits

Changed type returned from getUnitLiteral from Sequent to E
Change theorem 3.1

Statement was changed, proof was cleaned a bit