diff options
Diffstat (limited to 'theories/Wellfounded')
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 4 | ||||
| -rwxr-xr-x | theories/Wellfounded/intro.tex | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index a51b876ab..419f545f5 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -91,7 +91,7 @@ Section Wf_Symmetric_Product. Syntactic Definition Symprod := (symprod A B leA leB). -(* +(*i Local sig_prod:= [x:A*B]<{_:A&B}>Case x of [a:A][b:B](existS A [_:A]B a b) end. @@ -108,7 +108,7 @@ Proof. (Apply right_lex;Auto with sets). Save. -*) +i*) Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y) ->(Acc (A*B) Symprod (x,y)). diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex new file mode 100755 index 000000000..126071e28 --- /dev/null +++ b/theories/Wellfounded/intro.tex @@ -0,0 +1,4 @@ +\section{Well-founded relations}\label{Wellfounded} + +This library gives definitions and results about well-founded relations. + |