diff options
-rw-r--r-- | src/Util/MSetPositive/Facts.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Util/MSetPositive/Facts.v b/src/Util/MSetPositive/Facts.v index 26e2eadeb..3ccf5ad89 100644 --- a/src/Util/MSetPositive/Facts.v +++ b/src/Util/MSetPositive/Facts.v @@ -31,4 +31,19 @@ Module PositiveSetFacts. rewrite !elements_spec1. apply Hp. Qed. + + Lemma In_elements_mem_iff {x p} + : List.In x (elements p) <-> PositiveSet.mem x p = true. + Proof using Type. + rewrite elements_b, existsb_exists; cbv [eqb]. + repeat first [ apply conj + | progress intros + | progress destruct_head'_ex + | progress destruct_head'_and + | eexists + | eassumption + | break_innermost_match_step + | break_innermost_match_hyps_step + | congruence ]. + Qed. End PositiveSetFacts. |