@@ -385,7 +385,7 @@ The answer comes from the fact that Coq implements %\index{constructive logic}%_
Hencethedistinctionbetween[bool]and[Prop].Programsoftype[bool]arecomputationalbyconstruction;wecanalwaysrunthemtodeterminetheirresults.Many[Prop]sareundecidable,andsowecanwritemoreexpressiveformulaswith[Prop]sthanwith[bool]s,buttheinevitableconsequenceisthatwecannotsimply%``%#"#run a [Prop] to determine its truth.#"#%''%