Splitting of coherent idempotents
A counterexample: not every idempotent is coherent
fix nits in Idempotent.v
Merge pull request #635 from mikeshulman/idempotents

Splitting of coherent idempotents