diff options
| -rw-r--r-- | theories/Lists/List.v | 5 | ||||
| -rw-r--r-- | theories/Lists/SetoidList.v | 2 |
2 files changed, 6 insertions, 1 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index b3e37685bb..766456fff7 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -825,6 +825,11 @@ Section Map. rewrite IHl; auto. Qed. + Lemma map_eq_nil : forall l, map l = [] -> l = []. + Proof. + destruct l; simpl; reflexivity || discriminate. + Qed. + (** [flat_map] *) Definition flat_map (f:A -> list B) := diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 2aecb3fdbf..d42e71e556 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -489,7 +489,7 @@ left; auto. destruct IHl. left; auto. right; intro; inv; contradiction. -Qed. +Defined. Fixpoint removeA (x : A) (l : list A) : list A := match l with |