fullSimplify performs simple equational or equivalence transformations throughout the goal to simplify redundant expressions.
For example, 0*s simplifies to 0, P -> (P & Q) simplifies to P -> Q, and (in context) [a](P -> (P & Q)) simplifies to [a]P -> Q.
See also: