diff options
| author | Hugo Herbelin | 2020-09-09 13:45:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-09 13:45:04 +0200 |
| commit | 3d22134121ddeeb2052266d5f2cbcc097a5f0388 (patch) | |
| tree | 18dabcd54b2f45b83b9963be5174d940490ed514 /doc | |
| parent | 6f12c3e3ccce7028abb492f804d30ba0bef58f06 (diff) | |
| parent | f2ba2ad48dfa72f293702f4f86565b12f0302d4b (diff) | |
Merge PR #12094: Extend app_inj_tail and other list lemmas
Reviewed-by: anton-trunov
Ack-by: herbelin
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/12094-app_inj_tail.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/10-standard-library/12094-app_inj_tail.rst b/doc/changelog/10-standard-library/12094-app_inj_tail.rst new file mode 100644 index 0000000000..702fbb3d64 --- /dev/null +++ b/doc/changelog/10-standard-library/12094-app_inj_tail.rst @@ -0,0 +1,5 @@ +- **Added:** + Extend some list lemmas to both directions: `app_inj_tail_iff`, `app_inv_head_iff`, `app_inv_tail_iff`. + (`#12094 <https://github.com/coq/coq/pull/12094>`_, + fixes `#12093 <https://github.com/coq/coq/issues/12093>`_, + by Edward Wang). |