fixed typos
added more theorems about dpll
added some extra theorems in dpll.v and removed dpll-extra; resolution-based proofs are now in dpll-resolution.v