Textual Form of a Proof in Group Theory
Get the axioms of group theory, using CircleTimes as group product and 
as identity element. Group elements are represented by default as formal symbols a, b, c.
One of the axioms states existence of right identity. Prove the existence of left identity.
Get a human-readable form of the 11 steps of the proof.
Prove another theorem in group theory.
Show a graph of its steps, highlighting more important lemmas as bigger circles or triangles.
