diff options
Diffstat (limited to 'theories/Wellfounded/Lexicographic_Product.v')
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 4 |
1 files changed, 2 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)). |