proposition: Lemma not_In_all_but P ch : (~PositiveSet.In (pos_of_ascii ch) (all_but P)) <-> P ch.
proof: Proof. unfold all_but. setoid_rewrite PositiveSet.filter_spec; [ | congruence.. ]. setoid_rewrite (LogicFacts.True_iff (In_all ch)). rewrite ascii_of_pos_of_ascii. destruct (P ch); intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.MSets.MSetPositive Coq.Classes.Morphisms Fiat.Parsers.StringLike.FirstChar Fiat.Parsers.StringLike.LastChar Fiat.Parsers.StringLike.ForallChars Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.StringLike.Properties Fiat.Parsers.Splitters.RDPList Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Fix.FromAbstractInterpretationDefinitions Fiat.Parsers.ContextFreeGrammar.Fix.Fix Fiat.Parsers.ContextFreeGrammar.Fix.AsciiLattice Fiat.Parsers.ContextFreeGrammar.Fix.ProdAbstractInterpretationDefinitions Fiat.Parsers.ContextFreeGrammar.Fix.FromAbstractInterpretation Fiat.Parsers.Refinement.EmptyLemmas Fiat.Common.BoolFacts Fiat.Common.LogicFacts Fiat.Common.NatFacts Fiat.Common