diff options
Diffstat (limited to 'theories/Lists/PolyList.v')
| -rw-r--r-- | theories/Lists/PolyList.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index cd56ba1de..5baa76891 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -38,7 +38,8 @@ Fixpoint app [l:list] : list -> list | (cons a l1) => (cons a (app l1 m)) end. -Infix RIGHTA 7 "^" app. +Infix RIGHTA 7 "^" app + V8only 30. Lemma app_nil_end : (l:list)l=(l^nil). Proof. |