On 2020-09-24 16:15, mechvel at scico.botik.ru wrote: >> [..] > (1) A very simple problems. For example, to prove reverse (reverse xs) > == xs > for a list xs, > or to prove that _*_ in unary system for natural numbers is > commutative > (m * n == n * n). > [..] Fixing a typo: this should be (m * n == n * m). -- SM