diff options
| -rw-r--r-- | theories/Logic/Hurkens.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 06c72a4cb0..5f1d5232fa 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -38,8 +38,11 @@ - The [NoRetractFromTypeToProp] module proves that [Prop] cannot be a retract of a larger type. - - The [Prop_neq_Type] module proves that [Prop] is different from - any larger [Type]. + - The [TypeNeqSmallType] module proves that [Type] is different + from any smaller type. + + - The [PropNeqType] module proves that [Prop] is different from + any larger [Type]. It is an instance of the previous result. References: |