This article explained some internals of the logic system in coq. It answered questions like why is Type : Type consistent.

These tactics are sometimes useful. Here's an summary:

1. Timing is everything.
2. Always start with a blind quote.
3. Negotiate on the phone or in person.
4. Let them negotiate against themselves.
5. It really works like the movies.
6. Never save anyone.
7. Offer to pay up front and/or sign the papers today.
8. Don’t pay setup fees.
9. Negotiate for the long term.
10. Know when to stop.

I personally have been benefited from some of the tactics. It's an interesting find while I was dallying on the internet.