proposition: Lemma elements_find_iff elt kv (m : t elt) : List.In kv (elements m) <-> find (fst kv) m = Some (snd kv).
proof: Proof. destruct kv; symmetry; apply find_elements_iff. Qed.
imports: Coq.PArith.BinPos Coq.PArith.Pnat Coq.Arith.Arith Coq.FSets.FMapInterface Coq.FSets.FMapPositive Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.Prod