diff options
| author | Erik Martin-Dorel | 2019-02-27 17:31:35 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-03-20 12:54:26 +0100 |
| commit | c07f1f8d89dd1f975e06e8c45df2c7a4e6ca7fc3 (patch) | |
| tree | 73c109057bf3f18127be887fcc1b2e0ba82ff3e2 /mathcomp/ssreflect/finset.v | |
| parent | 4c8455594c5adff08761037a5919c058d0d502ba (diff) | |
Add extra eta lemmas for the under tactic
Related: coq/coq#9651
Diffstat (limited to 'mathcomp/ssreflect/finset.v')
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 87d5da4..20b3601 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -239,11 +239,15 @@ Proof. by rewrite in_set. Qed. Lemma eqsVneq A B : {A = B} + {A != B}. Proof. exact: eqVneq. Qed. +Lemma eq_finset (pA pB : pred T) : pA =1 pB -> finset pA = finset pB. +Proof. by move=> eq_p; apply/setP => x; rewrite !(in_set, inE) eq_p. Qed. + End BasicSetTheory. Definition inE := (in_set, inE). Arguments set0 {T}. +Arguments eq_finset {T} [pA] pB eq_pAB. Hint Resolve in_setT : core. Notation "[ 'set' : T ]" := (setTfor (Phant T)) @@ -2210,4 +2214,3 @@ Arguments setCK {T}. Arguments minsetP {T P A}. Arguments maxsetP {T P A}. Prenex Implicits minset maxset. - |