Add more, hopefully rather uncontroversial simplifications

[teiesti]

This is the first follow-up for #164. It groups all the "easy" and therefore rather "uncontroversial" simplifications.

[teiesti]

@ZachJHansen You can review and merge this whenever you like. I do not indent to add more to this. All other simplifications will go into other PRs.

[ZachJHansen]

Looks good overall, except I would prefer that each change in apply_definitions be a separate function so we can choose to apply them independently. Also, it would be nice to support a transformation from "F -> #false" to "not F" as well.

[teiesti]

We discussed in today's joint meeting:

1. We split apply_definitions into apply_negation_definition, apply_implication_definition and apply_equivalence_definition.
2. We add the inverse of each of these functions, e.g. apply_negation_definition_inverse.