We do not have special simplification rules for the equivalence operator. You have to expand it to a DNF or CNF for simplifications that you have in mind.
The X(back-arrow) is the previous operator, and in the case above, it is the weak version. It holds, if "a" holds at the previous point of time if there is one. The strong previous operator is false at initial time while the weak one (that you have here) is initially true.