On 2013-02-24 15:28, Serge D. Mechveliani wrote: > Can anybody demonstrate, please, how can this be (approximately) rewritten > by using EqReasoning, or may be, some other `reasoning' part of the > library? There are many examples of equational reasoning in the standard library. You could for instance take a look at Algebra.Props.BooleanAlgebra. -- /NAD