MathCheck Propositional Logic Problem

Prove that `harr` is associative. `(P harr Q) harr R hArr` has been given as the starting point. MathCheck only checks that the formulae are equivalent, not that the solution proceeds and ends reasonably. prop_logic

#(P<->Q#)<->R /**/ <=> end_of_answer

or