diff options
Diffstat (limited to 'theories/Sets/Permut.v')
| -rwxr-xr-x | theories/Sets/Permut.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index 686ea973e..03a8b7428 100755 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -10,8 +10,8 @@ (* G. Huet 1-9-95 *) -(* We consider a Set U, given with a commutative-associative operator op, -and a congruence cong; we show permutation lemmas *) +(** We consider a Set [U], given with a commutative-associative operator [op], + and a congruence [cong]; we show permutation lemmas *) Section Axiomatisation. @@ -29,7 +29,7 @@ Hypothesis cong_right : (x,y,z:U)(cong x y)->(cong (op z x) (op z y)). Hypothesis cong_trans : (x,y,z:U)(cong x y)->(cong y z)->(cong x z). Hypothesis cong_sym : (x,y:U)(cong x y)->(cong y x). -(* Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *) +(** Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *) Lemma cong_congr : (x,y,z,t:U)(cong x y)->(cong z t)->(cong (op x z) (op y t)). |