proposition: Lemma Empty_iff elt (m : t elt) : Empty m <-> PositiveMap.Empty m.
proof: Proof. unfold Empty, PositiveMap.Empty, key, MapsTo. rewrite forall_nonterminal_iffP. setoid_rewrite positive_to_nonterminal_to_positive; reflexivity. 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