Adds a .git ignore.
The symmetry property used for picking new names now using transpositions.

The previous version was incorrect. If ν is in the concretisation of a graph g, and ν' agrees with ν on all the nodes of g, it is still possible that ν' is not in the concretisation of g, if, for instance, g is a single inductive α.ι, and ν' concretises all the nodes on (ν α).
Removes a commented out piece of code.
Advances on the effective inductive summaries.

This is still very work in progress.