diff options
| -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 *) |