Better doc and a few fixes for Proof using.