diff options
| author | Olivier Laurent | 2019-10-30 22:34:27 +0100 |
|---|---|---|
| committer | Olivier Laurent | 2019-12-06 14:34:30 +0100 |
| commit | f2e42b1d902765f1ebacd410cc21b67ebfadcc6d (patch) | |
| tree | d18b0aa85da3826944f742418f92ec9b0780c4cc /theories/Lists | |
| parent | 84379df936b84d6394ce763193bd910c4f2be66c (diff) | |
integration of statements for rev
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/List.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 1478ea4f54..d0b4f61587 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -764,6 +764,12 @@ Section ListOps. rewrite IHl; auto. Qed. + Lemma rev_eq_app : forall l l1 l2, rev l = l1 ++ l2 -> l = rev l2 ++ rev l1. + Proof. + intros l l1 l2 Heq. + rewrite <- (rev_involutive l), Heq. + apply rev_app_distr. + Qed. (** Compatibility with other operations *) |