diff options
| -rw-r--r-- | theories/Lists/SetoidList.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 726f569d60..47f632d65f 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -228,6 +228,18 @@ Section Remove. Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. +Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }. +Proof. +induction l. +right; auto. +red; inversion 1. +destruct (eqA_dec x a). +left; auto. +destruct IHl. +left; auto. +right; red; inversion_clear 1; tauto. +Qed. + Fixpoint removeA (x : A) (l : list A){struct l} : list A := match l with | nil => nil |