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.