proposition: Lemma find_elements_iff : find x m = Some e <-> List.In (x, e) (elements m).
proof: Proof. split; intro H; [ apply elements_1_eq, find_2, H | apply find_1, elements_2_eq, H ]. 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