From 5da17aada0348ee9a8f7a238f015de96f2f507d5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Dec 2018 08:40:26 -0500 Subject: Add In_elements_mem_iff --- src/Util/MSetPositive/Facts.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'src/Util') 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. -- cgit v1.2.3