proposition: Lemma MapsTo_iff2 elt k v (m : t elt) : MapsTo (positive_to_nonterminal k) v m <-> PositiveMap.MapsTo k v m.
proof: Proof. unfold MapsTo. 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