diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
| commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
| tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /theories/Lists/SetoidPermutation.v | |
| parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) | |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'theories/Lists/SetoidPermutation.v')
| -rw-r--r-- | theories/Lists/SetoidPermutation.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v index b0657b63..afc7c25b 100644 --- a/theories/Lists/SetoidPermutation.v +++ b/theories/Lists/SetoidPermutation.v @@ -7,6 +7,7 @@ (***********************************************************************) Require Import SetoidList. +(* Set Universe Polymorphism. *) Set Implicit Arguments. Unset Strict Implicit. @@ -88,7 +89,7 @@ Lemma PermutationA_cons_app l l₁ l₂ x : PermutationA l (l₁ ++ l₂) -> PermutationA (x :: l) (l₁ ++ x :: l₂). Proof. intros E. rewrite E. - now rewrite app_comm_cons, PermutationA_cons_append, <-app_assoc. + now rewrite app_comm_cons, (PermutationA_cons_append l₁ x), <- app_assoc. Qed. Lemma PermutationA_middle l₁ l₂ x : |