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 /**/ <=>
or
This file was generated 2017-04-13 11:52:26 UTC.