Library CoLoR.Util.Logic.EpsilonUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2014-12-11
basic consequences of ClassicalEpsilon.constructive_indefinite_description

Set Implicit Arguments.



Notation cid := constructive_indefinite_description.