Description: Define the free group on a set I of generators, defined as the
quotient of the free monoid on I X. 2o (representing the generator
elements and their formal inverses) by the free group equivalence
relation df-efg . (Contributed by Mario Carneiro, 1-Oct-2015)