proposition: Lemma PositiveMap_elements_iff {A m k v} : @PositiveMap.find A k m = Some v <-> In (k, v) (PositiveMap.elements m).
proof: Proof. rewrite PositiveMapExtensions.elements_iff_find. rewrite InA_alt; unfold PositiveMap.eq_key_elt, PositiveMap.E.eq; simpl. split; [ intros [[? ?] [[? ?] ?]] | intro H; exists (k, v) ]; subst; repeat split; assumption. Qed.
imports: Coq.Init.Wf Coq.Numbers.BinNums Coq.Arith.Arith Coq.FSets.FMapPositive Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.Splitters.RDPList Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Fix.Definitions Fiat.Parsers.ContextFreeGrammar.Fix.Properties Fiat.Common.FMapExtensions.Wf Fiat.Common Fiat.Common.OptionFacts Fiat.Common.SetoidInstances