Better simplification of preconditions for eq_lemmas

Looking at the result of eq_lemmas after calling
``val _ = translation_extends "decProg";`` in the front of to_flatProgTheory
it seems some theorems stored have unnecessary T in the implication
```
T ⇒ EqualityType LISP_VALUES_LISP_V_TYPE
```
Another example of preconditions not being simplified.
```
⊢ T ⇒ EqualityType STRING_TYPE ⇒ EqualityType TERM_TYPE,
```
```
T ⇒
EqualityType NUM ⇒
EqualityType STRING_TYPE ⇒
EqualityType TERM_TYPE ⇒
EqualityType (LIST_TYPE (PAIR_TYPE STRING_TYPE TERM_TYPE)) ⇒
EqualityType UPDATE_TYPE
```