(macro) show the generated equivalence relation maintained at the current subterm

General Forms:
geneqv     ; show list of equivalence relations being maintained
(geneqv t) ; as above, but pair each relation with a justifying rune

This is an advanced command, whose effect is to print the so-called ``generated equivalence relation'' (or ``geneqv'') that is maintained at the current subterm of the conclusion. That structure is a list of equivalence relations, representing the transitive closure E of the union of those relations, such that it suffices to maintain E at the current subterm: if that subterm, u, is replaced in the goal's conclusion, G, by another term equivalent to u with respect to E, then the resulting conclusion is Boolean equivalent to G. Also see defcong.

The command `geneqv' prints the above list of equivalence relations, or more precisely, the list of function symbols for those relations. If however geneqv is given a non-nil argument, then a list is printed whose elements are each of the form (s r), where s is the symbol for an equivalence relation and r is a :congruence rune justifying the inclusion of s in the list of equivalence relations being maintained at the current subterm.