Why library for Coq

 This package contains all useful logical definitions, lemmas with their
 proofs and axioms used by Why. Users may need this package when proving
 some proof obligations in Coq.