diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 7c38a54ea..611782b4f 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1450,7 +1450,7 @@ a logical property of a computational object. In the same spirit, elimination on $P$ of type $I\ra \Type$ cannot be allowed because it trivially implies the elimination on $P$ of type $I\ra \Set$ by cumulativity. It also implies that there -is two proofs of the same property which are provably different, +are two proofs of the same property which are provably different, contradicting the proof-irrelevance property which is sometimes a useful axiom: \begin{coq_example} |