proposition: Lemma positive_to_nonterminal_to_positive nt : nonterminal_to_positive (positive_to_nonterminal nt) = nt.
proof: Proof. unfold nonterminal_to_positive, positive_to_nonterminal. erewrite Nat.lt_succ_pred by apply Pos2Nat.is_pos. rewrite Pos2Nat.id. 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