proposition: Lemma ascii_mem v (H : MSetPositive.PositiveSet.cardinal v = 1) ch' (H' : MSetPositive.PositiveSet.choose v = Some ch') (Hch' : pos_of_ascii (Ascii.ascii_of_pos ch') = ch') ch'' (Hch'' : Ascii.ascii_of_pos ch' = ch'') ch : MSetPositive.PositiveSet.mem (pos_of_ascii ch) v = Equality.ascii_beq ch'' ch.
proof: Proof. apply MSetPositive.PositiveSet.choose_spec1 in H'. destruct (Equality.ascii_beq ch'' ch) eqn:Hch; subst ch''. { apply Equality.ascii_bl in Hch; subst ch. AsciiLattice.PositiveSetExtensions.BasicDec.fsetdec. } { AsciiLattice.PositiveSetExtensions.to_caps. intro; apply Hch; clear Hch. apply Equality.ascii_beq_true_iff. rewrite <- ascii_of_pos_of_ascii; apply f_equal. eapply AsciiLattice.PositiveSetExtensions.cardinal_one_In_same; eassumption. } 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