I am new to Ghilbert and this mailing list. The concept sounds very interesting, and I have a few questions. Please pardon me if I am missing obvious points.
The Ghilbert home page mentions replacing distinct variable conditions with a more traditional technique for expressing free variable conditions. This sounds attractive in that free variable conditions are much more familiar. I have two questions about this:
1) Have you found some proofs that are significantly harder or more cumbersome using the more traditional approach? (If so can you refer me to a couple in some way?)
2) Does the system currently have a way to specify the conditions (and is there documentation that I may have overlooked)?
I know the system is far from complete, but this is an interesting topic from my point of view.